The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, INF).

(0) Obligation:

Runtime Complexity Relative TRS:
The TRS R consists of the following rules:

#abs(#0) → #0
#abs(#neg(@x)) → #pos(@x)
#abs(#pos(@x)) → #pos(@x)
#abs(#s(@x)) → #pos(#s(@x))
*(@x, @y) → #mult(@x, @y)
+(@x, @y) → #add(@x, @y)
attach(@line, @m) → attach#1(@line, @m)
attach#1(::(@x, @xs), @m) → attach#2(@m, @x, @xs)
attach#1(nil, @m) → nil
attach#2(::(@l, @ls), @x, @xs) → ::(::(@x, @l), attach(@xs, @ls))
attach#2(nil, @x, @xs) → nil
lineMult(@l, @m2) → lineMult#1(@m2, @l)
lineMult#1(::(@x, @xs), @l) → ::(mult(@l, @x), lineMult(@l, @xs))
lineMult#1(nil, @l) → nil
m1(@x) → ::(::(#abs(#pos(#s(#0))), ::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#0))))), nil))), ::(::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#0))))), ::(#abs(#pos(#s(#s(#s(#s(#0)))))), nil))), nil))
m2(@x) → ::(::(#abs(#pos(#s(#0))), ::(#abs(#pos(#s(#s(#0)))), nil)), ::(::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#0))))), nil)), ::(::(#abs(#pos(#s(#s(#s(#s(#0)))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#0))))))), nil)), nil)))
m3(@x) → ::(::(#abs(#pos(#s(#0))), ::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#0))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#0))))))), nil)))), ::(::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#0))))), ::(#abs(#pos(#s(#s(#s(#s(#0)))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#0))))))), nil)))), nil))
m4(@x) → ::(::(#abs(#pos(#s(#0))), nil), ::(::(#abs(#pos(#s(#s(#0)))), nil), ::(::(#abs(#pos(#s(#s(#s(#0))))), nil), ::(::(#abs(#pos(#s(#s(#s(#s(#0)))))), nil), nil))))
makeBase(@m) → makeBase#1(@m)
makeBase#1(::(@l, @m')) → mkBase(@l)
makeBase#1(nil) → nil
matrixMult(@m1, @m2) → matrixMult'(@m1, transAcc(@m2, makeBase(@m2)))
matrixMult'(@m1, @m2) → matrixMult'#1(@m1, @m2)
matrixMult'#1(::(@l, @ls), @m2) → ::(lineMult(@l, @m2), matrixMult'(@ls, @m2))
matrixMult'#1(nil, @m2) → nil
matrixMult3(@m1, @m2, @m3) → matrixMult(matrixMult(@m1, @m2), @m3)
matrixMultList(@acc, @mm) → matrixMultList#1(@mm, @acc)
matrixMultList#1(::(@m, @ms), @acc) → matrixMultList(matrixMult(@acc, @m), @ms)
matrixMultList#1(nil, @acc) → @acc
matrixMultOld(@m1, @m2) → matrixMult'(@m1, transpose(@m2))
mkBase(@m) → mkBase#1(@m)
mkBase#1(::(@l, @m')) → ::(nil, mkBase(@m'))
mkBase#1(nil) → nil
mult(@l1, @l2) → mult#1(@l1, @l2)
mult#1(::(@x, @xs), @l2) → mult#2(@l2, @x, @xs)
mult#1(nil, @l2) → #abs(#0)
mult#2(::(@y, @ys), @x, @xs) → +(*(@x, @y), mult(@xs, @ys))
mult#2(nil, @x, @xs) → #abs(#0)
split(@m) → split#1(@m)
split#1(::(@l, @ls)) → split#2(@l, @ls)
split#1(nil) → tuple#2(nil, nil)
split#2(::(@x, @xs), @ls) → split#3(split(@ls), @x, @xs)
split#2(nil, @ls) → tuple#2(nil, nil)
split#3(tuple#2(@ys, @m'), @x, @xs) → tuple#2(::(@x, @ys), ::(@xs, @m'))
transAcc(@m, @base) → transAcc#1(@m, @base)
transAcc#1(::(@l, @m'), @base) → attach(@l, transAcc(@m', @base))
transAcc#1(nil, @base) → @base
transpose(@m) → transpose#1(@m, @m)
transpose#1(::(@xs, @xss), @m) → transpose#2(split(@m))
transpose#1(nil, @m) → nil
transpose#2(tuple#2(@l, @m')) → transpose#3(@m', @l)
transpose#3(::(@y, @ys), @l) → ::(@l, transpose(::(@y, @ys)))
transpose#3(nil, @l) → nil
transpose'(@m) → transAcc(@m, makeBase(@m))

The (relative) TRS S consists of the following rules:

#add(#0, @y) → @y
#add(#neg(#s(#0)), @y) → #pred(@y)
#add(#neg(#s(#s(@x))), @y) → #pred(#add(#pos(#s(@x)), @y))
#add(#pos(#s(#0)), @y) → #succ(@y)
#add(#pos(#s(#s(@x))), @y) → #succ(#add(#pos(#s(@x)), @y))
#mult(#0, #0) → #0
#mult(#0, #neg(@y)) → #0
#mult(#0, #pos(@y)) → #0
#mult(#neg(@x), #0) → #0
#mult(#neg(@x), #neg(@y)) → #pos(#natmult(@x, @y))
#mult(#neg(@x), #pos(@y)) → #neg(#natmult(@x, @y))
#mult(#pos(@x), #0) → #0
#mult(#pos(@x), #neg(@y)) → #neg(#natmult(@x, @y))
#mult(#pos(@x), #pos(@y)) → #pos(#natmult(@x, @y))
#natmult(#0, @y) → #0
#natmult(#s(@x), @y) → #add(#pos(@y), #natmult(@x, @y))
#pred(#0) → #neg(#s(#0))
#pred(#neg(#s(@x))) → #neg(#s(#s(@x)))
#pred(#pos(#s(#0))) → #0
#pred(#pos(#s(#s(@x)))) → #pos(#s(@x))
#succ(#0) → #pos(#s(#0))
#succ(#neg(#s(#0))) → #0
#succ(#neg(#s(#s(@x)))) → #neg(#s(@x))
#succ(#pos(#s(@x))) → #pos(#s(#s(@x)))

Rewrite Strategy: INNERMOST

(1) DecreasingLoopProof (EQUIVALENT transformation)

The following loop(s) give(s) rise to the lower bound Ω(n¹):
The rewrite sequence
attach(::(@x453639_5, @xs453640_5), ::(@l453764_5, @ls453765_5)) →⁺ ::(::(@x453639_5, @l453764_5), attach(@xs453640_5, @ls453765_5))
gives rise to a decreasing loop by considering the right hand sides subterm at position [1].
The pumping substitution is [@xs453640_5 / ::(@x453639_5, @xs453640_5), @ls453765_5 / ::(@l453764_5, @ls453765_5)].
The result substitution is [ ].

(2) BOUNDS(n^1, INF)

(3) RenamingProof (EQUIVALENT transformation)

Renamed function symbols to avoid clashes with predefined symbol.

(4) Obligation:

Runtime Complexity Relative TRS:
The TRS R consists of the following rules:

#abs(#0) → #0
#abs(#neg(@x)) → #pos(@x)
#abs(#pos(@x)) → #pos(@x)
#abs(#s(@x)) → #pos(#s(@x))
*'(@x, @y) → #mult(@x, @y)
+'(@x, @y) → #add(@x, @y)
attach(@line, @m) → attach#1(@line, @m)
attach#1(::(@x, @xs), @m) → attach#2(@m, @x, @xs)
attach#1(nil, @m) → nil
attach#2(::(@l, @ls), @x, @xs) → ::(::(@x, @l), attach(@xs, @ls))
attach#2(nil, @x, @xs) → nil
lineMult(@l, @m2) → lineMult#1(@m2, @l)
lineMult#1(::(@x, @xs), @l) → ::(mult(@l, @x), lineMult(@l, @xs))
lineMult#1(nil, @l) → nil
m1(@x) → ::(::(#abs(#pos(#s(#0))), ::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#0))))), nil))), ::(::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#0))))), ::(#abs(#pos(#s(#s(#s(#s(#0)))))), nil))), nil))
m2(@x) → ::(::(#abs(#pos(#s(#0))), ::(#abs(#pos(#s(#s(#0)))), nil)), ::(::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#0))))), nil)), ::(::(#abs(#pos(#s(#s(#s(#s(#0)))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#0))))))), nil)), nil)))
m3(@x) → ::(::(#abs(#pos(#s(#0))), ::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#0))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#0))))))), nil)))), ::(::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#0))))), ::(#abs(#pos(#s(#s(#s(#s(#0)))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#0))))))), nil)))), nil))
m4(@x) → ::(::(#abs(#pos(#s(#0))), nil), ::(::(#abs(#pos(#s(#s(#0)))), nil), ::(::(#abs(#pos(#s(#s(#s(#0))))), nil), ::(::(#abs(#pos(#s(#s(#s(#s(#0)))))), nil), nil))))
makeBase(@m) → makeBase#1(@m)
makeBase#1(::(@l, @m')) → mkBase(@l)
makeBase#1(nil) → nil
matrixMult(@m1, @m2) → matrixMult'(@m1, transAcc(@m2, makeBase(@m2)))
matrixMult'(@m1, @m2) → matrixMult'#1(@m1, @m2)
matrixMult'#1(::(@l, @ls), @m2) → ::(lineMult(@l, @m2), matrixMult'(@ls, @m2))
matrixMult'#1(nil, @m2) → nil
matrixMult3(@m1, @m2, @m3) → matrixMult(matrixMult(@m1, @m2), @m3)
matrixMultList(@acc, @mm) → matrixMultList#1(@mm, @acc)
matrixMultList#1(::(@m, @ms), @acc) → matrixMultList(matrixMult(@acc, @m), @ms)
matrixMultList#1(nil, @acc) → @acc
matrixMultOld(@m1, @m2) → matrixMult'(@m1, transpose(@m2))
mkBase(@m) → mkBase#1(@m)
mkBase#1(::(@l, @m')) → ::(nil, mkBase(@m'))
mkBase#1(nil) → nil
mult(@l1, @l2) → mult#1(@l1, @l2)
mult#1(::(@x, @xs), @l2) → mult#2(@l2, @x, @xs)
mult#1(nil, @l2) → #abs(#0)
mult#2(::(@y, @ys), @x, @xs) → +'(*'(@x, @y), mult(@xs, @ys))
mult#2(nil, @x, @xs) → #abs(#0)
split(@m) → split#1(@m)
split#1(::(@l, @ls)) → split#2(@l, @ls)
split#1(nil) → tuple#2(nil, nil)
split#2(::(@x, @xs), @ls) → split#3(split(@ls), @x, @xs)
split#2(nil, @ls) → tuple#2(nil, nil)
split#3(tuple#2(@ys, @m'), @x, @xs) → tuple#2(::(@x, @ys), ::(@xs, @m'))
transAcc(@m, @base) → transAcc#1(@m, @base)
transAcc#1(::(@l, @m'), @base) → attach(@l, transAcc(@m', @base))
transAcc#1(nil, @base) → @base
transpose(@m) → transpose#1(@m, @m)
transpose#1(::(@xs, @xss), @m) → transpose#2(split(@m))
transpose#1(nil, @m) → nil
transpose#2(tuple#2(@l, @m')) → transpose#3(@m', @l)
transpose#3(::(@y, @ys), @l) → ::(@l, transpose(::(@y, @ys)))
transpose#3(nil, @l) → nil
transpose'(@m) → transAcc(@m, makeBase(@m))

The (relative) TRS S consists of the following rules:

#add(#0, @y) → @y
#add(#neg(#s(#0)), @y) → #pred(@y)
#add(#neg(#s(#s(@x))), @y) → #pred(#add(#pos(#s(@x)), @y))
#add(#pos(#s(#0)), @y) → #succ(@y)
#add(#pos(#s(#s(@x))), @y) → #succ(#add(#pos(#s(@x)), @y))
#mult(#0, #0) → #0
#mult(#0, #neg(@y)) → #0
#mult(#0, #pos(@y)) → #0
#mult(#neg(@x), #0) → #0
#mult(#neg(@x), #neg(@y)) → #pos(#natmult(@x, @y))
#mult(#neg(@x), #pos(@y)) → #neg(#natmult(@x, @y))
#mult(#pos(@x), #0) → #0
#mult(#pos(@x), #neg(@y)) → #neg(#natmult(@x, @y))
#mult(#pos(@x), #pos(@y)) → #pos(#natmult(@x, @y))
#natmult(#0, @y) → #0
#natmult(#s(@x), @y) → #add(#pos(@y), #natmult(@x, @y))
#pred(#0) → #neg(#s(#0))
#pred(#neg(#s(@x))) → #neg(#s(#s(@x)))
#pred(#pos(#s(#0))) → #0
#pred(#pos(#s(#s(@x)))) → #pos(#s(@x))
#succ(#0) → #pos(#s(#0))
#succ(#neg(#s(#0))) → #0
#succ(#neg(#s(#s(@x)))) → #neg(#s(@x))
#succ(#pos(#s(@x))) → #pos(#s(#s(@x)))

Rewrite Strategy: INNERMOST

(5) SlicingProof (LOWER BOUND(ID) transformation)

Sliced the following arguments:
m1/0
m2/0
m3/0
m4/0

(6) Obligation:

Runtime Complexity Relative TRS:
The TRS R consists of the following rules:

#abs(#0) → #0
#abs(#neg(@x)) → #pos(@x)
#abs(#pos(@x)) → #pos(@x)
#abs(#s(@x)) → #pos(#s(@x))
*'(@x, @y) → #mult(@x, @y)
+'(@x, @y) → #add(@x, @y)
attach(@line, @m) → attach#1(@line, @m)
attach#1(::(@x, @xs), @m) → attach#2(@m, @x, @xs)
attach#1(nil, @m) → nil
attach#2(::(@l, @ls), @x, @xs) → ::(::(@x, @l), attach(@xs, @ls))
attach#2(nil, @x, @xs) → nil
lineMult(@l, @m2) → lineMult#1(@m2, @l)
lineMult#1(::(@x, @xs), @l) → ::(mult(@l, @x), lineMult(@l, @xs))
lineMult#1(nil, @l) → nil
m1 → ::(::(#abs(#pos(#s(#0))), ::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#0))))), nil))), ::(::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#0))))), ::(#abs(#pos(#s(#s(#s(#s(#0)))))), nil))), nil))
m2 → ::(::(#abs(#pos(#s(#0))), ::(#abs(#pos(#s(#s(#0)))), nil)), ::(::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#0))))), nil)), ::(::(#abs(#pos(#s(#s(#s(#s(#0)))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#0))))))), nil)), nil)))
m3 → ::(::(#abs(#pos(#s(#0))), ::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#0))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#0))))))), nil)))), ::(::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#0))))), ::(#abs(#pos(#s(#s(#s(#s(#0)))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#0))))))), nil)))), nil))
m4 → ::(::(#abs(#pos(#s(#0))), nil), ::(::(#abs(#pos(#s(#s(#0)))), nil), ::(::(#abs(#pos(#s(#s(#s(#0))))), nil), ::(::(#abs(#pos(#s(#s(#s(#s(#0)))))), nil), nil))))
makeBase(@m) → makeBase#1(@m)
makeBase#1(::(@l, @m')) → mkBase(@l)
makeBase#1(nil) → nil
matrixMult(@m1, @m2) → matrixMult'(@m1, transAcc(@m2, makeBase(@m2)))
matrixMult'(@m1, @m2) → matrixMult'#1(@m1, @m2)
matrixMult'#1(::(@l, @ls), @m2) → ::(lineMult(@l, @m2), matrixMult'(@ls, @m2))
matrixMult'#1(nil, @m2) → nil
matrixMult3(@m1, @m2, @m3) → matrixMult(matrixMult(@m1, @m2), @m3)
matrixMultList(@acc, @mm) → matrixMultList#1(@mm, @acc)
matrixMultList#1(::(@m, @ms), @acc) → matrixMultList(matrixMult(@acc, @m), @ms)
matrixMultList#1(nil, @acc) → @acc
matrixMultOld(@m1, @m2) → matrixMult'(@m1, transpose(@m2))
mkBase(@m) → mkBase#1(@m)
mkBase#1(::(@l, @m')) → ::(nil, mkBase(@m'))
mkBase#1(nil) → nil
mult(@l1, @l2) → mult#1(@l1, @l2)
mult#1(::(@x, @xs), @l2) → mult#2(@l2, @x, @xs)
mult#1(nil, @l2) → #abs(#0)
mult#2(::(@y, @ys), @x, @xs) → +'(*'(@x, @y), mult(@xs, @ys))
mult#2(nil, @x, @xs) → #abs(#0)
split(@m) → split#1(@m)
split#1(::(@l, @ls)) → split#2(@l, @ls)
split#1(nil) → tuple#2(nil, nil)
split#2(::(@x, @xs), @ls) → split#3(split(@ls), @x, @xs)
split#2(nil, @ls) → tuple#2(nil, nil)
split#3(tuple#2(@ys, @m'), @x, @xs) → tuple#2(::(@x, @ys), ::(@xs, @m'))
transAcc(@m, @base) → transAcc#1(@m, @base)
transAcc#1(::(@l, @m'), @base) → attach(@l, transAcc(@m', @base))
transAcc#1(nil, @base) → @base
transpose(@m) → transpose#1(@m, @m)
transpose#1(::(@xs, @xss), @m) → transpose#2(split(@m))
transpose#1(nil, @m) → nil
transpose#2(tuple#2(@l, @m')) → transpose#3(@m', @l)
transpose#3(::(@y, @ys), @l) → ::(@l, transpose(::(@y, @ys)))
transpose#3(nil, @l) → nil
transpose'(@m) → transAcc(@m, makeBase(@m))

The (relative) TRS S consists of the following rules:

#add(#0, @y) → @y
#add(#neg(#s(#0)), @y) → #pred(@y)
#add(#neg(#s(#s(@x))), @y) → #pred(#add(#pos(#s(@x)), @y))
#add(#pos(#s(#0)), @y) → #succ(@y)
#add(#pos(#s(#s(@x))), @y) → #succ(#add(#pos(#s(@x)), @y))
#mult(#0, #0) → #0
#mult(#0, #neg(@y)) → #0
#mult(#0, #pos(@y)) → #0
#mult(#neg(@x), #0) → #0
#mult(#neg(@x), #neg(@y)) → #pos(#natmult(@x, @y))
#mult(#neg(@x), #pos(@y)) → #neg(#natmult(@x, @y))
#mult(#pos(@x), #0) → #0
#mult(#pos(@x), #neg(@y)) → #neg(#natmult(@x, @y))
#mult(#pos(@x), #pos(@y)) → #pos(#natmult(@x, @y))
#natmult(#0, @y) → #0
#natmult(#s(@x), @y) → #add(#pos(@y), #natmult(@x, @y))
#pred(#0) → #neg(#s(#0))
#pred(#neg(#s(@x))) → #neg(#s(#s(@x)))
#pred(#pos(#s(#0))) → #0
#pred(#pos(#s(#s(@x)))) → #pos(#s(@x))
#succ(#0) → #pos(#s(#0))
#succ(#neg(#s(#0))) → #0
#succ(#neg(#s(#s(@x)))) → #neg(#s(@x))
#succ(#pos(#s(@x))) → #pos(#s(#s(@x)))

Rewrite Strategy: INNERMOST

(7) TypeInferenceProof (BOTH BOUNDS(ID, ID) transformation)

Infered types.

(8) Obligation:

Innermost TRS:
Rules:
#abs(#0) → #0
#abs(#neg(@x)) → #pos(@x)
#abs(#pos(@x)) → #pos(@x)
#abs(#s(@x)) → #pos(#s(@x))
*'(@x, @y) → #mult(@x, @y)
+'(@x, @y) → #add(@x, @y)
attach(@line, @m) → attach#1(@line, @m)
attach#1(::(@x, @xs), @m) → attach#2(@m, @x, @xs)
attach#1(nil, @m) → nil
attach#2(::(@l, @ls), @x, @xs) → ::(::(@x, @l), attach(@xs, @ls))
attach#2(nil, @x, @xs) → nil
lineMult(@l, @m2) → lineMult#1(@m2, @l)
lineMult#1(::(@x, @xs), @l) → ::(mult(@l, @x), lineMult(@l, @xs))
lineMult#1(nil, @l) → nil
m1 → ::(::(#abs(#pos(#s(#0))), ::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#0))))), nil))), ::(::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#0))))), ::(#abs(#pos(#s(#s(#s(#s(#0)))))), nil))), nil))
m2 → ::(::(#abs(#pos(#s(#0))), ::(#abs(#pos(#s(#s(#0)))), nil)), ::(::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#0))))), nil)), ::(::(#abs(#pos(#s(#s(#s(#s(#0)))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#0))))))), nil)), nil)))
m3 → ::(::(#abs(#pos(#s(#0))), ::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#0))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#0))))))), nil)))), ::(::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#0))))), ::(#abs(#pos(#s(#s(#s(#s(#0)))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#0))))))), nil)))), nil))
m4 → ::(::(#abs(#pos(#s(#0))), nil), ::(::(#abs(#pos(#s(#s(#0)))), nil), ::(::(#abs(#pos(#s(#s(#s(#0))))), nil), ::(::(#abs(#pos(#s(#s(#s(#s(#0)))))), nil), nil))))
makeBase(@m) → makeBase#1(@m)
makeBase#1(::(@l, @m')) → mkBase(@l)
makeBase#1(nil) → nil
matrixMult(@m1, @m2) → matrixMult'(@m1, transAcc(@m2, makeBase(@m2)))
matrixMult'(@m1, @m2) → matrixMult'#1(@m1, @m2)
matrixMult'#1(::(@l, @ls), @m2) → ::(lineMult(@l, @m2), matrixMult'(@ls, @m2))
matrixMult'#1(nil, @m2) → nil
matrixMult3(@m1, @m2, @m3) → matrixMult(matrixMult(@m1, @m2), @m3)
matrixMultList(@acc, @mm) → matrixMultList#1(@mm, @acc)
matrixMultList#1(::(@m, @ms), @acc) → matrixMultList(matrixMult(@acc, @m), @ms)
matrixMultList#1(nil, @acc) → @acc
matrixMultOld(@m1, @m2) → matrixMult'(@m1, transpose(@m2))
mkBase(@m) → mkBase#1(@m)
mkBase#1(::(@l, @m')) → ::(nil, mkBase(@m'))
mkBase#1(nil) → nil
mult(@l1, @l2) → mult#1(@l1, @l2)
mult#1(::(@x, @xs), @l2) → mult#2(@l2, @x, @xs)
mult#1(nil, @l2) → #abs(#0)
mult#2(::(@y, @ys), @x, @xs) → +'(*'(@x, @y), mult(@xs, @ys))
mult#2(nil, @x, @xs) → #abs(#0)
split(@m) → split#1(@m)
split#1(::(@l, @ls)) → split#2(@l, @ls)
split#1(nil) → tuple#2(nil, nil)
split#2(::(@x, @xs), @ls) → split#3(split(@ls), @x, @xs)
split#2(nil, @ls) → tuple#2(nil, nil)
split#3(tuple#2(@ys, @m'), @x, @xs) → tuple#2(::(@x, @ys), ::(@xs, @m'))
transAcc(@m, @base) → transAcc#1(@m, @base)
transAcc#1(::(@l, @m'), @base) → attach(@l, transAcc(@m', @base))
transAcc#1(nil, @base) → @base
transpose(@m) → transpose#1(@m, @m)
transpose#1(::(@xs, @xss), @m) → transpose#2(split(@m))
transpose#1(nil, @m) → nil
transpose#2(tuple#2(@l, @m')) → transpose#3(@m', @l)
transpose#3(::(@y, @ys), @l) → ::(@l, transpose(::(@y, @ys)))
transpose#3(nil, @l) → nil
transpose'(@m) → transAcc(@m, makeBase(@m))
#add(#0, @y) → @y
#add(#neg(#s(#0)), @y) → #pred(@y)
#add(#neg(#s(#s(@x))), @y) → #pred(#add(#pos(#s(@x)), @y))
#add(#pos(#s(#0)), @y) → #succ(@y)
#add(#pos(#s(#s(@x))), @y) → #succ(#add(#pos(#s(@x)), @y))
#mult(#0, #0) → #0
#mult(#0, #neg(@y)) → #0
#mult(#0, #pos(@y)) → #0
#mult(#neg(@x), #0) → #0
#mult(#neg(@x), #neg(@y)) → #pos(#natmult(@x, @y))
#mult(#neg(@x), #pos(@y)) → #neg(#natmult(@x, @y))
#mult(#pos(@x), #0) → #0
#mult(#pos(@x), #neg(@y)) → #neg(#natmult(@x, @y))
#mult(#pos(@x), #pos(@y)) → #pos(#natmult(@x, @y))
#natmult(#0, @y) → #0
#natmult(#s(@x), @y) → #add(#pos(@y), #natmult(@x, @y))
#pred(#0) → #neg(#s(#0))
#pred(#neg(#s(@x))) → #neg(#s(#s(@x)))
#pred(#pos(#s(#0))) → #0
#pred(#pos(#s(#s(@x)))) → #pos(#s(@x))
#succ(#0) → #pos(#s(#0))
#succ(#neg(#s(#0))) → #0
#succ(#neg(#s(#s(@x)))) → #neg(#s(@x))
#succ(#pos(#s(@x))) → #pos(#s(#s(@x)))

Types:
#abs :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
#0 :: #0:#neg:#pos:#s::::nil
#neg :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
#pos :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
#s :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
*' :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
#mult :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
+' :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
#add :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
attach :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
attach#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
:: :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
attach#2 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
nil :: #0:#neg:#pos:#s::::nil
lineMult :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
lineMult#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
mult :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
m1 :: #0:#neg:#pos:#s::::nil
m2 :: #0:#neg:#pos:#s::::nil
m3 :: #0:#neg:#pos:#s::::nil
m4 :: #0:#neg:#pos:#s::::nil
makeBase :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
makeBase#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
mkBase :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
matrixMult :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
matrixMult' :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
transAcc :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
matrixMult'#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
matrixMult3 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
matrixMultList :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
matrixMultList#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
matrixMultOld :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
transpose :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
mkBase#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
mult#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
mult#2 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
split :: #0:#neg:#pos:#s::::nil → tuple#2
split#1 :: #0:#neg:#pos:#s::::nil → tuple#2
split#2 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → tuple#2
tuple#2 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → tuple#2
split#3 :: tuple#2 → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → tuple#2
transAcc#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
transpose#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
transpose#2 :: tuple#2 → #0:#neg:#pos:#s::::nil
transpose#3 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
transpose' :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
#pred :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
#succ :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
#natmult :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
hole_#0:#neg:#pos:#s::::nil1_5 :: #0:#neg:#pos:#s::::nil
hole_tuple#22_5 :: tuple#2
gen_#0:#neg:#pos:#s::::nil3_5 :: Nat → #0:#neg:#pos:#s::::nil

(9) OrderProof (LOWER BOUND(ID) transformation)

Heuristically decided to analyse the following defined symbols:
#add, attach, attach#1, lineMult, lineMult#1, mult, mkBase, matrixMult', transAcc, matrixMult'#1, matrixMultList, matrixMultList#1, transpose, mkBase#1, mult#1, split, split#1, transAcc#1, transpose#2, #natmult

They will be analysed ascendingly in the following order:
#add < #natmult
attach = attach#1
attach < transAcc#1
lineMult = lineMult#1
lineMult < matrixMult'#1
mult < lineMult#1
mult = mult#1
mkBase = mkBase#1
matrixMult' = matrixMult'#1
transAcc = transAcc#1
matrixMultList = matrixMultList#1
split < transpose
transpose = transpose#2
split = split#1

(10) Obligation:

Innermost TRS:
Rules:
#abs(#0) → #0
#abs(#neg(@x)) → #pos(@x)
#abs(#pos(@x)) → #pos(@x)
#abs(#s(@x)) → #pos(#s(@x))
*'(@x, @y) → #mult(@x, @y)
+'(@x, @y) → #add(@x, @y)
attach(@line, @m) → attach#1(@line, @m)
attach#1(::(@x, @xs), @m) → attach#2(@m, @x, @xs)
attach#1(nil, @m) → nil
attach#2(::(@l, @ls), @x, @xs) → ::(::(@x, @l), attach(@xs, @ls))
attach#2(nil, @x, @xs) → nil
lineMult(@l, @m2) → lineMult#1(@m2, @l)
lineMult#1(::(@x, @xs), @l) → ::(mult(@l, @x), lineMult(@l, @xs))
lineMult#1(nil, @l) → nil
m1 → ::(::(#abs(#pos(#s(#0))), ::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#0))))), nil))), ::(::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#0))))), ::(#abs(#pos(#s(#s(#s(#s(#0)))))), nil))), nil))
m2 → ::(::(#abs(#pos(#s(#0))), ::(#abs(#pos(#s(#s(#0)))), nil)), ::(::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#0))))), nil)), ::(::(#abs(#pos(#s(#s(#s(#s(#0)))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#0))))))), nil)), nil)))
m3 → ::(::(#abs(#pos(#s(#0))), ::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#0))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#0))))))), nil)))), ::(::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#0))))), ::(#abs(#pos(#s(#s(#s(#s(#0)))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#0))))))), nil)))), nil))
m4 → ::(::(#abs(#pos(#s(#0))), nil), ::(::(#abs(#pos(#s(#s(#0)))), nil), ::(::(#abs(#pos(#s(#s(#s(#0))))), nil), ::(::(#abs(#pos(#s(#s(#s(#s(#0)))))), nil), nil))))
makeBase(@m) → makeBase#1(@m)
makeBase#1(::(@l, @m')) → mkBase(@l)
makeBase#1(nil) → nil
matrixMult(@m1, @m2) → matrixMult'(@m1, transAcc(@m2, makeBase(@m2)))
matrixMult'(@m1, @m2) → matrixMult'#1(@m1, @m2)
matrixMult'#1(::(@l, @ls), @m2) → ::(lineMult(@l, @m2), matrixMult'(@ls, @m2))
matrixMult'#1(nil, @m2) → nil
matrixMult3(@m1, @m2, @m3) → matrixMult(matrixMult(@m1, @m2), @m3)
matrixMultList(@acc, @mm) → matrixMultList#1(@mm, @acc)
matrixMultList#1(::(@m, @ms), @acc) → matrixMultList(matrixMult(@acc, @m), @ms)
matrixMultList#1(nil, @acc) → @acc
matrixMultOld(@m1, @m2) → matrixMult'(@m1, transpose(@m2))
mkBase(@m) → mkBase#1(@m)
mkBase#1(::(@l, @m')) → ::(nil, mkBase(@m'))
mkBase#1(nil) → nil
mult(@l1, @l2) → mult#1(@l1, @l2)
mult#1(::(@x, @xs), @l2) → mult#2(@l2, @x, @xs)
mult#1(nil, @l2) → #abs(#0)
mult#2(::(@y, @ys), @x, @xs) → +'(*'(@x, @y), mult(@xs, @ys))
mult#2(nil, @x, @xs) → #abs(#0)
split(@m) → split#1(@m)
split#1(::(@l, @ls)) → split#2(@l, @ls)
split#1(nil) → tuple#2(nil, nil)
split#2(::(@x, @xs), @ls) → split#3(split(@ls), @x, @xs)
split#2(nil, @ls) → tuple#2(nil, nil)
split#3(tuple#2(@ys, @m'), @x, @xs) → tuple#2(::(@x, @ys), ::(@xs, @m'))
transAcc(@m, @base) → transAcc#1(@m, @base)
transAcc#1(::(@l, @m'), @base) → attach(@l, transAcc(@m', @base))
transAcc#1(nil, @base) → @base
transpose(@m) → transpose#1(@m, @m)
transpose#1(::(@xs, @xss), @m) → transpose#2(split(@m))
transpose#1(nil, @m) → nil
transpose#2(tuple#2(@l, @m')) → transpose#3(@m', @l)
transpose#3(::(@y, @ys), @l) → ::(@l, transpose(::(@y, @ys)))
transpose#3(nil, @l) → nil
transpose'(@m) → transAcc(@m, makeBase(@m))
#add(#0, @y) → @y
#add(#neg(#s(#0)), @y) → #pred(@y)
#add(#neg(#s(#s(@x))), @y) → #pred(#add(#pos(#s(@x)), @y))
#add(#pos(#s(#0)), @y) → #succ(@y)
#add(#pos(#s(#s(@x))), @y) → #succ(#add(#pos(#s(@x)), @y))
#mult(#0, #0) → #0
#mult(#0, #neg(@y)) → #0
#mult(#0, #pos(@y)) → #0
#mult(#neg(@x), #0) → #0
#mult(#neg(@x), #neg(@y)) → #pos(#natmult(@x, @y))
#mult(#neg(@x), #pos(@y)) → #neg(#natmult(@x, @y))
#mult(#pos(@x), #0) → #0
#mult(#pos(@x), #neg(@y)) → #neg(#natmult(@x, @y))
#mult(#pos(@x), #pos(@y)) → #pos(#natmult(@x, @y))
#natmult(#0, @y) → #0
#natmult(#s(@x), @y) → #add(#pos(@y), #natmult(@x, @y))
#pred(#0) → #neg(#s(#0))
#pred(#neg(#s(@x))) → #neg(#s(#s(@x)))
#pred(#pos(#s(#0))) → #0
#pred(#pos(#s(#s(@x)))) → #pos(#s(@x))
#succ(#0) → #pos(#s(#0))
#succ(#neg(#s(#0))) → #0
#succ(#neg(#s(#s(@x)))) → #neg(#s(@x))
#succ(#pos(#s(@x))) → #pos(#s(#s(@x)))

Types:
#abs :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
#0 :: #0:#neg:#pos:#s::::nil
#neg :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
#pos :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
#s :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
*' :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
#mult :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
+' :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
#add :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
attach :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
attach#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
:: :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
attach#2 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
nil :: #0:#neg:#pos:#s::::nil
lineMult :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
lineMult#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
mult :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
m1 :: #0:#neg:#pos:#s::::nil
m2 :: #0:#neg:#pos:#s::::nil
m3 :: #0:#neg:#pos:#s::::nil
m4 :: #0:#neg:#pos:#s::::nil
makeBase :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
makeBase#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
mkBase :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
matrixMult :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
matrixMult' :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
transAcc :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
matrixMult'#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
matrixMult3 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
matrixMultList :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
matrixMultList#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
matrixMultOld :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
transpose :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
mkBase#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
mult#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
mult#2 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
split :: #0:#neg:#pos:#s::::nil → tuple#2
split#1 :: #0:#neg:#pos:#s::::nil → tuple#2
split#2 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → tuple#2
tuple#2 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → tuple#2
split#3 :: tuple#2 → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → tuple#2
transAcc#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
transpose#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
transpose#2 :: tuple#2 → #0:#neg:#pos:#s::::nil
transpose#3 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
transpose' :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
#pred :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
#succ :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
#natmult :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
hole_#0:#neg:#pos:#s::::nil1_5 :: #0:#neg:#pos:#s::::nil
hole_tuple#22_5 :: tuple#2
gen_#0:#neg:#pos:#s::::nil3_5 :: Nat → #0:#neg:#pos:#s::::nil

Generator Equations:
gen_#0:#neg:#pos:#s::::nil3_5(0) ⇔ #0
gen_#0:#neg:#pos:#s::::nil3_5(+(x, 1)) ⇔ #neg(gen_#0:#neg:#pos:#s::::nil3_5(x))

The following defined symbols remain to be analysed:
#add, attach, attach#1, lineMult, lineMult#1, mult, mkBase, matrixMult', transAcc, matrixMult'#1, matrixMultList, matrixMultList#1, transpose, mkBase#1, mult#1, split, split#1, transAcc#1, transpose#2, #natmult

They will be analysed ascendingly in the following order:
#add < #natmult
attach = attach#1
attach < transAcc#1
lineMult = lineMult#1
lineMult < matrixMult'#1
mult < lineMult#1
mult = mult#1
mkBase = mkBase#1
matrixMult' = matrixMult'#1
transAcc = transAcc#1
matrixMultList = matrixMultList#1
split < transpose
transpose = transpose#2
split = split#1

(11) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol #add.

(12) Obligation:

Innermost TRS:
Rules:
#abs(#0) → #0
#abs(#neg(@x)) → #pos(@x)
#abs(#pos(@x)) → #pos(@x)
#abs(#s(@x)) → #pos(#s(@x))
*'(@x, @y) → #mult(@x, @y)
+'(@x, @y) → #add(@x, @y)
attach(@line, @m) → attach#1(@line, @m)
attach#1(::(@x, @xs), @m) → attach#2(@m, @x, @xs)
attach#1(nil, @m) → nil
attach#2(::(@l, @ls), @x, @xs) → ::(::(@x, @l), attach(@xs, @ls))
attach#2(nil, @x, @xs) → nil
lineMult(@l, @m2) → lineMult#1(@m2, @l)
lineMult#1(::(@x, @xs), @l) → ::(mult(@l, @x), lineMult(@l, @xs))
lineMult#1(nil, @l) → nil
m1 → ::(::(#abs(#pos(#s(#0))), ::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#0))))), nil))), ::(::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#0))))), ::(#abs(#pos(#s(#s(#s(#s(#0)))))), nil))), nil))
m2 → ::(::(#abs(#pos(#s(#0))), ::(#abs(#pos(#s(#s(#0)))), nil)), ::(::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#0))))), nil)), ::(::(#abs(#pos(#s(#s(#s(#s(#0)))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#0))))))), nil)), nil)))
m3 → ::(::(#abs(#pos(#s(#0))), ::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#0))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#0))))))), nil)))), ::(::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#0))))), ::(#abs(#pos(#s(#s(#s(#s(#0)))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#0))))))), nil)))), nil))
m4 → ::(::(#abs(#pos(#s(#0))), nil), ::(::(#abs(#pos(#s(#s(#0)))), nil), ::(::(#abs(#pos(#s(#s(#s(#0))))), nil), ::(::(#abs(#pos(#s(#s(#s(#s(#0)))))), nil), nil))))
makeBase(@m) → makeBase#1(@m)
makeBase#1(::(@l, @m')) → mkBase(@l)
makeBase#1(nil) → nil
matrixMult(@m1, @m2) → matrixMult'(@m1, transAcc(@m2, makeBase(@m2)))
matrixMult'(@m1, @m2) → matrixMult'#1(@m1, @m2)
matrixMult'#1(::(@l, @ls), @m2) → ::(lineMult(@l, @m2), matrixMult'(@ls, @m2))
matrixMult'#1(nil, @m2) → nil
matrixMult3(@m1, @m2, @m3) → matrixMult(matrixMult(@m1, @m2), @m3)
matrixMultList(@acc, @mm) → matrixMultList#1(@mm, @acc)
matrixMultList#1(::(@m, @ms), @acc) → matrixMultList(matrixMult(@acc, @m), @ms)
matrixMultList#1(nil, @acc) → @acc
matrixMultOld(@m1, @m2) → matrixMult'(@m1, transpose(@m2))
mkBase(@m) → mkBase#1(@m)
mkBase#1(::(@l, @m')) → ::(nil, mkBase(@m'))
mkBase#1(nil) → nil
mult(@l1, @l2) → mult#1(@l1, @l2)
mult#1(::(@x, @xs), @l2) → mult#2(@l2, @x, @xs)
mult#1(nil, @l2) → #abs(#0)
mult#2(::(@y, @ys), @x, @xs) → +'(*'(@x, @y), mult(@xs, @ys))
mult#2(nil, @x, @xs) → #abs(#0)
split(@m) → split#1(@m)
split#1(::(@l, @ls)) → split#2(@l, @ls)
split#1(nil) → tuple#2(nil, nil)
split#2(::(@x, @xs), @ls) → split#3(split(@ls), @x, @xs)
split#2(nil, @ls) → tuple#2(nil, nil)
split#3(tuple#2(@ys, @m'), @x, @xs) → tuple#2(::(@x, @ys), ::(@xs, @m'))
transAcc(@m, @base) → transAcc#1(@m, @base)
transAcc#1(::(@l, @m'), @base) → attach(@l, transAcc(@m', @base))
transAcc#1(nil, @base) → @base
transpose(@m) → transpose#1(@m, @m)
transpose#1(::(@xs, @xss), @m) → transpose#2(split(@m))
transpose#1(nil, @m) → nil
transpose#2(tuple#2(@l, @m')) → transpose#3(@m', @l)
transpose#3(::(@y, @ys), @l) → ::(@l, transpose(::(@y, @ys)))
transpose#3(nil, @l) → nil
transpose'(@m) → transAcc(@m, makeBase(@m))
#add(#0, @y) → @y
#add(#neg(#s(#0)), @y) → #pred(@y)
#add(#neg(#s(#s(@x))), @y) → #pred(#add(#pos(#s(@x)), @y))
#add(#pos(#s(#0)), @y) → #succ(@y)
#add(#pos(#s(#s(@x))), @y) → #succ(#add(#pos(#s(@x)), @y))
#mult(#0, #0) → #0
#mult(#0, #neg(@y)) → #0
#mult(#0, #pos(@y)) → #0
#mult(#neg(@x), #0) → #0
#mult(#neg(@x), #neg(@y)) → #pos(#natmult(@x, @y))
#mult(#neg(@x), #pos(@y)) → #neg(#natmult(@x, @y))
#mult(#pos(@x), #0) → #0
#mult(#pos(@x), #neg(@y)) → #neg(#natmult(@x, @y))
#mult(#pos(@x), #pos(@y)) → #pos(#natmult(@x, @y))
#natmult(#0, @y) → #0
#natmult(#s(@x), @y) → #add(#pos(@y), #natmult(@x, @y))
#pred(#0) → #neg(#s(#0))
#pred(#neg(#s(@x))) → #neg(#s(#s(@x)))
#pred(#pos(#s(#0))) → #0
#pred(#pos(#s(#s(@x)))) → #pos(#s(@x))
#succ(#0) → #pos(#s(#0))
#succ(#neg(#s(#0))) → #0
#succ(#neg(#s(#s(@x)))) → #neg(#s(@x))
#succ(#pos(#s(@x))) → #pos(#s(#s(@x)))

Types:
#abs :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
#0 :: #0:#neg:#pos:#s::::nil
#neg :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
#pos :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
#s :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
*' :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
#mult :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
+' :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
#add :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
attach :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
attach#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
:: :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
attach#2 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
nil :: #0:#neg:#pos:#s::::nil
lineMult :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
lineMult#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
mult :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
m1 :: #0:#neg:#pos:#s::::nil
m2 :: #0:#neg:#pos:#s::::nil
m3 :: #0:#neg:#pos:#s::::nil
m4 :: #0:#neg:#pos:#s::::nil
makeBase :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
makeBase#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
mkBase :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
matrixMult :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
matrixMult' :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
transAcc :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
matrixMult'#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
matrixMult3 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
matrixMultList :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
matrixMultList#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
matrixMultOld :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
transpose :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
mkBase#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
mult#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
mult#2 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
split :: #0:#neg:#pos:#s::::nil → tuple#2
split#1 :: #0:#neg:#pos:#s::::nil → tuple#2
split#2 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → tuple#2
tuple#2 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → tuple#2
split#3 :: tuple#2 → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → tuple#2
transAcc#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
transpose#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
transpose#2 :: tuple#2 → #0:#neg:#pos:#s::::nil
transpose#3 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
transpose' :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
#pred :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
#succ :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
#natmult :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
hole_#0:#neg:#pos:#s::::nil1_5 :: #0:#neg:#pos:#s::::nil
hole_tuple#22_5 :: tuple#2
gen_#0:#neg:#pos:#s::::nil3_5 :: Nat → #0:#neg:#pos:#s::::nil

Generator Equations:
gen_#0:#neg:#pos:#s::::nil3_5(0) ⇔ #0
gen_#0:#neg:#pos:#s::::nil3_5(+(x, 1)) ⇔ #neg(gen_#0:#neg:#pos:#s::::nil3_5(x))

The following defined symbols remain to be analysed:
#natmult, attach, attach#1, lineMult, lineMult#1, mult, mkBase, matrixMult', transAcc, matrixMult'#1, matrixMultList, matrixMultList#1, transpose, mkBase#1, mult#1, split, split#1, transAcc#1, transpose#2

They will be analysed ascendingly in the following order:
attach = attach#1
attach < transAcc#1
lineMult = lineMult#1
lineMult < matrixMult'#1
mult < lineMult#1
mult = mult#1
mkBase = mkBase#1
matrixMult' = matrixMult'#1
transAcc = transAcc#1
matrixMultList = matrixMultList#1
split < transpose
transpose = transpose#2
split = split#1

(13) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol #natmult.

(14) Obligation:

Innermost TRS:
Rules:
#abs(#0) → #0
#abs(#neg(@x)) → #pos(@x)
#abs(#pos(@x)) → #pos(@x)
#abs(#s(@x)) → #pos(#s(@x))
*'(@x, @y) → #mult(@x, @y)
+'(@x, @y) → #add(@x, @y)
attach(@line, @m) → attach#1(@line, @m)
attach#1(::(@x, @xs), @m) → attach#2(@m, @x, @xs)
attach#1(nil, @m) → nil
attach#2(::(@l, @ls), @x, @xs) → ::(::(@x, @l), attach(@xs, @ls))
attach#2(nil, @x, @xs) → nil
lineMult(@l, @m2) → lineMult#1(@m2, @l)
lineMult#1(::(@x, @xs), @l) → ::(mult(@l, @x), lineMult(@l, @xs))
lineMult#1(nil, @l) → nil
m1 → ::(::(#abs(#pos(#s(#0))), ::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#0))))), nil))), ::(::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#0))))), ::(#abs(#pos(#s(#s(#s(#s(#0)))))), nil))), nil))
m2 → ::(::(#abs(#pos(#s(#0))), ::(#abs(#pos(#s(#s(#0)))), nil)), ::(::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#0))))), nil)), ::(::(#abs(#pos(#s(#s(#s(#s(#0)))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#0))))))), nil)), nil)))
m3 → ::(::(#abs(#pos(#s(#0))), ::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#0))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#0))))))), nil)))), ::(::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#0))))), ::(#abs(#pos(#s(#s(#s(#s(#0)))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#0))))))), nil)))), nil))
m4 → ::(::(#abs(#pos(#s(#0))), nil), ::(::(#abs(#pos(#s(#s(#0)))), nil), ::(::(#abs(#pos(#s(#s(#s(#0))))), nil), ::(::(#abs(#pos(#s(#s(#s(#s(#0)))))), nil), nil))))
makeBase(@m) → makeBase#1(@m)
makeBase#1(::(@l, @m')) → mkBase(@l)
makeBase#1(nil) → nil
matrixMult(@m1, @m2) → matrixMult'(@m1, transAcc(@m2, makeBase(@m2)))
matrixMult'(@m1, @m2) → matrixMult'#1(@m1, @m2)
matrixMult'#1(::(@l, @ls), @m2) → ::(lineMult(@l, @m2), matrixMult'(@ls, @m2))
matrixMult'#1(nil, @m2) → nil
matrixMult3(@m1, @m2, @m3) → matrixMult(matrixMult(@m1, @m2), @m3)
matrixMultList(@acc, @mm) → matrixMultList#1(@mm, @acc)
matrixMultList#1(::(@m, @ms), @acc) → matrixMultList(matrixMult(@acc, @m), @ms)
matrixMultList#1(nil, @acc) → @acc
matrixMultOld(@m1, @m2) → matrixMult'(@m1, transpose(@m2))
mkBase(@m) → mkBase#1(@m)
mkBase#1(::(@l, @m')) → ::(nil, mkBase(@m'))
mkBase#1(nil) → nil
mult(@l1, @l2) → mult#1(@l1, @l2)
mult#1(::(@x, @xs), @l2) → mult#2(@l2, @x, @xs)
mult#1(nil, @l2) → #abs(#0)
mult#2(::(@y, @ys), @x, @xs) → +'(*'(@x, @y), mult(@xs, @ys))
mult#2(nil, @x, @xs) → #abs(#0)
split(@m) → split#1(@m)
split#1(::(@l, @ls)) → split#2(@l, @ls)
split#1(nil) → tuple#2(nil, nil)
split#2(::(@x, @xs), @ls) → split#3(split(@ls), @x, @xs)
split#2(nil, @ls) → tuple#2(nil, nil)
split#3(tuple#2(@ys, @m'), @x, @xs) → tuple#2(::(@x, @ys), ::(@xs, @m'))
transAcc(@m, @base) → transAcc#1(@m, @base)
transAcc#1(::(@l, @m'), @base) → attach(@l, transAcc(@m', @base))
transAcc#1(nil, @base) → @base
transpose(@m) → transpose#1(@m, @m)
transpose#1(::(@xs, @xss), @m) → transpose#2(split(@m))
transpose#1(nil, @m) → nil
transpose#2(tuple#2(@l, @m')) → transpose#3(@m', @l)
transpose#3(::(@y, @ys), @l) → ::(@l, transpose(::(@y, @ys)))
transpose#3(nil, @l) → nil
transpose'(@m) → transAcc(@m, makeBase(@m))
#add(#0, @y) → @y
#add(#neg(#s(#0)), @y) → #pred(@y)
#add(#neg(#s(#s(@x))), @y) → #pred(#add(#pos(#s(@x)), @y))
#add(#pos(#s(#0)), @y) → #succ(@y)
#add(#pos(#s(#s(@x))), @y) → #succ(#add(#pos(#s(@x)), @y))
#mult(#0, #0) → #0
#mult(#0, #neg(@y)) → #0
#mult(#0, #pos(@y)) → #0
#mult(#neg(@x), #0) → #0
#mult(#neg(@x), #neg(@y)) → #pos(#natmult(@x, @y))
#mult(#neg(@x), #pos(@y)) → #neg(#natmult(@x, @y))
#mult(#pos(@x), #0) → #0
#mult(#pos(@x), #neg(@y)) → #neg(#natmult(@x, @y))
#mult(#pos(@x), #pos(@y)) → #pos(#natmult(@x, @y))
#natmult(#0, @y) → #0
#natmult(#s(@x), @y) → #add(#pos(@y), #natmult(@x, @y))
#pred(#0) → #neg(#s(#0))
#pred(#neg(#s(@x))) → #neg(#s(#s(@x)))
#pred(#pos(#s(#0))) → #0
#pred(#pos(#s(#s(@x)))) → #pos(#s(@x))
#succ(#0) → #pos(#s(#0))
#succ(#neg(#s(#0))) → #0
#succ(#neg(#s(#s(@x)))) → #neg(#s(@x))
#succ(#pos(#s(@x))) → #pos(#s(#s(@x)))

Types:
#abs :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
#0 :: #0:#neg:#pos:#s::::nil
#neg :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
#pos :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
#s :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
*' :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
#mult :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
+' :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
#add :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
attach :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
attach#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
:: :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
attach#2 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
nil :: #0:#neg:#pos:#s::::nil
lineMult :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
lineMult#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
mult :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
m1 :: #0:#neg:#pos:#s::::nil
m2 :: #0:#neg:#pos:#s::::nil
m3 :: #0:#neg:#pos:#s::::nil
m4 :: #0:#neg:#pos:#s::::nil
makeBase :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
makeBase#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
mkBase :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
matrixMult :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
matrixMult' :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
transAcc :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
matrixMult'#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
matrixMult3 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
matrixMultList :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
matrixMultList#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
matrixMultOld :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
transpose :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
mkBase#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
mult#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
mult#2 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
split :: #0:#neg:#pos:#s::::nil → tuple#2
split#1 :: #0:#neg:#pos:#s::::nil → tuple#2
split#2 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → tuple#2
tuple#2 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → tuple#2
split#3 :: tuple#2 → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → tuple#2
transAcc#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
transpose#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
transpose#2 :: tuple#2 → #0:#neg:#pos:#s::::nil
transpose#3 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
transpose' :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
#pred :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
#succ :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
#natmult :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
hole_#0:#neg:#pos:#s::::nil1_5 :: #0:#neg:#pos:#s::::nil
hole_tuple#22_5 :: tuple#2
gen_#0:#neg:#pos:#s::::nil3_5 :: Nat → #0:#neg:#pos:#s::::nil

Generator Equations:
gen_#0:#neg:#pos:#s::::nil3_5(0) ⇔ #0
gen_#0:#neg:#pos:#s::::nil3_5(+(x, 1)) ⇔ #neg(gen_#0:#neg:#pos:#s::::nil3_5(x))

The following defined symbols remain to be analysed:
split#1, attach, attach#1, lineMult, lineMult#1, mult, mkBase, matrixMult', transAcc, matrixMult'#1, matrixMultList, matrixMultList#1, transpose, mkBase#1, mult#1, split, transAcc#1, transpose#2

They will be analysed ascendingly in the following order:
attach = attach#1
attach < transAcc#1
lineMult = lineMult#1
lineMult < matrixMult'#1
mult < lineMult#1
mult = mult#1
mkBase = mkBase#1
matrixMult' = matrixMult'#1
transAcc = transAcc#1
matrixMultList = matrixMultList#1
split < transpose
transpose = transpose#2
split = split#1

(15) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol split#1.

(16) Obligation:

Innermost TRS:
Rules:
#abs(#0) → #0
#abs(#neg(@x)) → #pos(@x)
#abs(#pos(@x)) → #pos(@x)
#abs(#s(@x)) → #pos(#s(@x))
*'(@x, @y) → #mult(@x, @y)
+'(@x, @y) → #add(@x, @y)
attach(@line, @m) → attach#1(@line, @m)
attach#1(::(@x, @xs), @m) → attach#2(@m, @x, @xs)
attach#1(nil, @m) → nil
attach#2(::(@l, @ls), @x, @xs) → ::(::(@x, @l), attach(@xs, @ls))
attach#2(nil, @x, @xs) → nil
lineMult(@l, @m2) → lineMult#1(@m2, @l)
lineMult#1(::(@x, @xs), @l) → ::(mult(@l, @x), lineMult(@l, @xs))
lineMult#1(nil, @l) → nil
m1 → ::(::(#abs(#pos(#s(#0))), ::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#0))))), nil))), ::(::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#0))))), ::(#abs(#pos(#s(#s(#s(#s(#0)))))), nil))), nil))
m2 → ::(::(#abs(#pos(#s(#0))), ::(#abs(#pos(#s(#s(#0)))), nil)), ::(::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#0))))), nil)), ::(::(#abs(#pos(#s(#s(#s(#s(#0)))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#0))))))), nil)), nil)))
m3 → ::(::(#abs(#pos(#s(#0))), ::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#0))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#0))))))), nil)))), ::(::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#0))))), ::(#abs(#pos(#s(#s(#s(#s(#0)))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#0))))))), nil)))), nil))
m4 → ::(::(#abs(#pos(#s(#0))), nil), ::(::(#abs(#pos(#s(#s(#0)))), nil), ::(::(#abs(#pos(#s(#s(#s(#0))))), nil), ::(::(#abs(#pos(#s(#s(#s(#s(#0)))))), nil), nil))))
makeBase(@m) → makeBase#1(@m)
makeBase#1(::(@l, @m')) → mkBase(@l)
makeBase#1(nil) → nil
matrixMult(@m1, @m2) → matrixMult'(@m1, transAcc(@m2, makeBase(@m2)))
matrixMult'(@m1, @m2) → matrixMult'#1(@m1, @m2)
matrixMult'#1(::(@l, @ls), @m2) → ::(lineMult(@l, @m2), matrixMult'(@ls, @m2))
matrixMult'#1(nil, @m2) → nil
matrixMult3(@m1, @m2, @m3) → matrixMult(matrixMult(@m1, @m2), @m3)
matrixMultList(@acc, @mm) → matrixMultList#1(@mm, @acc)
matrixMultList#1(::(@m, @ms), @acc) → matrixMultList(matrixMult(@acc, @m), @ms)
matrixMultList#1(nil, @acc) → @acc
matrixMultOld(@m1, @m2) → matrixMult'(@m1, transpose(@m2))
mkBase(@m) → mkBase#1(@m)
mkBase#1(::(@l, @m')) → ::(nil, mkBase(@m'))
mkBase#1(nil) → nil
mult(@l1, @l2) → mult#1(@l1, @l2)
mult#1(::(@x, @xs), @l2) → mult#2(@l2, @x, @xs)
mult#1(nil, @l2) → #abs(#0)
mult#2(::(@y, @ys), @x, @xs) → +'(*'(@x, @y), mult(@xs, @ys))
mult#2(nil, @x, @xs) → #abs(#0)
split(@m) → split#1(@m)
split#1(::(@l, @ls)) → split#2(@l, @ls)
split#1(nil) → tuple#2(nil, nil)
split#2(::(@x, @xs), @ls) → split#3(split(@ls), @x, @xs)
split#2(nil, @ls) → tuple#2(nil, nil)
split#3(tuple#2(@ys, @m'), @x, @xs) → tuple#2(::(@x, @ys), ::(@xs, @m'))
transAcc(@m, @base) → transAcc#1(@m, @base)
transAcc#1(::(@l, @m'), @base) → attach(@l, transAcc(@m', @base))
transAcc#1(nil, @base) → @base
transpose(@m) → transpose#1(@m, @m)
transpose#1(::(@xs, @xss), @m) → transpose#2(split(@m))
transpose#1(nil, @m) → nil
transpose#2(tuple#2(@l, @m')) → transpose#3(@m', @l)
transpose#3(::(@y, @ys), @l) → ::(@l, transpose(::(@y, @ys)))
transpose#3(nil, @l) → nil
transpose'(@m) → transAcc(@m, makeBase(@m))
#add(#0, @y) → @y
#add(#neg(#s(#0)), @y) → #pred(@y)
#add(#neg(#s(#s(@x))), @y) → #pred(#add(#pos(#s(@x)), @y))
#add(#pos(#s(#0)), @y) → #succ(@y)
#add(#pos(#s(#s(@x))), @y) → #succ(#add(#pos(#s(@x)), @y))
#mult(#0, #0) → #0
#mult(#0, #neg(@y)) → #0
#mult(#0, #pos(@y)) → #0
#mult(#neg(@x), #0) → #0
#mult(#neg(@x), #neg(@y)) → #pos(#natmult(@x, @y))
#mult(#neg(@x), #pos(@y)) → #neg(#natmult(@x, @y))
#mult(#pos(@x), #0) → #0
#mult(#pos(@x), #neg(@y)) → #neg(#natmult(@x, @y))
#mult(#pos(@x), #pos(@y)) → #pos(#natmult(@x, @y))
#natmult(#0, @y) → #0
#natmult(#s(@x), @y) → #add(#pos(@y), #natmult(@x, @y))
#pred(#0) → #neg(#s(#0))
#pred(#neg(#s(@x))) → #neg(#s(#s(@x)))
#pred(#pos(#s(#0))) → #0
#pred(#pos(#s(#s(@x)))) → #pos(#s(@x))
#succ(#0) → #pos(#s(#0))
#succ(#neg(#s(#0))) → #0
#succ(#neg(#s(#s(@x)))) → #neg(#s(@x))
#succ(#pos(#s(@x))) → #pos(#s(#s(@x)))

Types:
#abs :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
#0 :: #0:#neg:#pos:#s::::nil
#neg :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
#pos :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
#s :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
*' :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
#mult :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
+' :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
#add :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
attach :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
attach#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
:: :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
attach#2 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
nil :: #0:#neg:#pos:#s::::nil
lineMult :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
lineMult#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
mult :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
m1 :: #0:#neg:#pos:#s::::nil
m2 :: #0:#neg:#pos:#s::::nil
m3 :: #0:#neg:#pos:#s::::nil
m4 :: #0:#neg:#pos:#s::::nil
makeBase :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
makeBase#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
mkBase :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
matrixMult :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
matrixMult' :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
transAcc :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
matrixMult'#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
matrixMult3 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
matrixMultList :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
matrixMultList#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
matrixMultOld :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
transpose :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
mkBase#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
mult#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
mult#2 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
split :: #0:#neg:#pos:#s::::nil → tuple#2
split#1 :: #0:#neg:#pos:#s::::nil → tuple#2
split#2 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → tuple#2
tuple#2 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → tuple#2
split#3 :: tuple#2 → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → tuple#2
transAcc#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
transpose#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
transpose#2 :: tuple#2 → #0:#neg:#pos:#s::::nil
transpose#3 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
transpose' :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
#pred :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
#succ :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
#natmult :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
hole_#0:#neg:#pos:#s::::nil1_5 :: #0:#neg:#pos:#s::::nil
hole_tuple#22_5 :: tuple#2
gen_#0:#neg:#pos:#s::::nil3_5 :: Nat → #0:#neg:#pos:#s::::nil

Generator Equations:
gen_#0:#neg:#pos:#s::::nil3_5(0) ⇔ #0
gen_#0:#neg:#pos:#s::::nil3_5(+(x, 1)) ⇔ #neg(gen_#0:#neg:#pos:#s::::nil3_5(x))

The following defined symbols remain to be analysed:
split, attach, attach#1, lineMult, lineMult#1, mult, mkBase, matrixMult', transAcc, matrixMult'#1, matrixMultList, matrixMultList#1, transpose, mkBase#1, mult#1, transAcc#1, transpose#2

They will be analysed ascendingly in the following order:
attach = attach#1
attach < transAcc#1
lineMult = lineMult#1
lineMult < matrixMult'#1
mult < lineMult#1
mult = mult#1
mkBase = mkBase#1
matrixMult' = matrixMult'#1
transAcc = transAcc#1
matrixMultList = matrixMultList#1
split < transpose
transpose = transpose#2
split = split#1

(17) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol split.

(18) Obligation:

Innermost TRS:
Rules:
#abs(#0) → #0
#abs(#neg(@x)) → #pos(@x)
#abs(#pos(@x)) → #pos(@x)
#abs(#s(@x)) → #pos(#s(@x))
*'(@x, @y) → #mult(@x, @y)
+'(@x, @y) → #add(@x, @y)
attach(@line, @m) → attach#1(@line, @m)
attach#1(::(@x, @xs), @m) → attach#2(@m, @x, @xs)
attach#1(nil, @m) → nil
attach#2(::(@l, @ls), @x, @xs) → ::(::(@x, @l), attach(@xs, @ls))
attach#2(nil, @x, @xs) → nil
lineMult(@l, @m2) → lineMult#1(@m2, @l)
lineMult#1(::(@x, @xs), @l) → ::(mult(@l, @x), lineMult(@l, @xs))
lineMult#1(nil, @l) → nil
m1 → ::(::(#abs(#pos(#s(#0))), ::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#0))))), nil))), ::(::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#0))))), ::(#abs(#pos(#s(#s(#s(#s(#0)))))), nil))), nil))
m2 → ::(::(#abs(#pos(#s(#0))), ::(#abs(#pos(#s(#s(#0)))), nil)), ::(::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#0))))), nil)), ::(::(#abs(#pos(#s(#s(#s(#s(#0)))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#0))))))), nil)), nil)))
m3 → ::(::(#abs(#pos(#s(#0))), ::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#0))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#0))))))), nil)))), ::(::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#0))))), ::(#abs(#pos(#s(#s(#s(#s(#0)))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#0))))))), nil)))), nil))
m4 → ::(::(#abs(#pos(#s(#0))), nil), ::(::(#abs(#pos(#s(#s(#0)))), nil), ::(::(#abs(#pos(#s(#s(#s(#0))))), nil), ::(::(#abs(#pos(#s(#s(#s(#s(#0)))))), nil), nil))))
makeBase(@m) → makeBase#1(@m)
makeBase#1(::(@l, @m')) → mkBase(@l)
makeBase#1(nil) → nil
matrixMult(@m1, @m2) → matrixMult'(@m1, transAcc(@m2, makeBase(@m2)))
matrixMult'(@m1, @m2) → matrixMult'#1(@m1, @m2)
matrixMult'#1(::(@l, @ls), @m2) → ::(lineMult(@l, @m2), matrixMult'(@ls, @m2))
matrixMult'#1(nil, @m2) → nil
matrixMult3(@m1, @m2, @m3) → matrixMult(matrixMult(@m1, @m2), @m3)
matrixMultList(@acc, @mm) → matrixMultList#1(@mm, @acc)
matrixMultList#1(::(@m, @ms), @acc) → matrixMultList(matrixMult(@acc, @m), @ms)
matrixMultList#1(nil, @acc) → @acc
matrixMultOld(@m1, @m2) → matrixMult'(@m1, transpose(@m2))
mkBase(@m) → mkBase#1(@m)
mkBase#1(::(@l, @m')) → ::(nil, mkBase(@m'))
mkBase#1(nil) → nil
mult(@l1, @l2) → mult#1(@l1, @l2)
mult#1(::(@x, @xs), @l2) → mult#2(@l2, @x, @xs)
mult#1(nil, @l2) → #abs(#0)
mult#2(::(@y, @ys), @x, @xs) → +'(*'(@x, @y), mult(@xs, @ys))
mult#2(nil, @x, @xs) → #abs(#0)
split(@m) → split#1(@m)
split#1(::(@l, @ls)) → split#2(@l, @ls)
split#1(nil) → tuple#2(nil, nil)
split#2(::(@x, @xs), @ls) → split#3(split(@ls), @x, @xs)
split#2(nil, @ls) → tuple#2(nil, nil)
split#3(tuple#2(@ys, @m'), @x, @xs) → tuple#2(::(@x, @ys), ::(@xs, @m'))
transAcc(@m, @base) → transAcc#1(@m, @base)
transAcc#1(::(@l, @m'), @base) → attach(@l, transAcc(@m', @base))
transAcc#1(nil, @base) → @base
transpose(@m) → transpose#1(@m, @m)
transpose#1(::(@xs, @xss), @m) → transpose#2(split(@m))
transpose#1(nil, @m) → nil
transpose#2(tuple#2(@l, @m')) → transpose#3(@m', @l)
transpose#3(::(@y, @ys), @l) → ::(@l, transpose(::(@y, @ys)))
transpose#3(nil, @l) → nil
transpose'(@m) → transAcc(@m, makeBase(@m))
#add(#0, @y) → @y
#add(#neg(#s(#0)), @y) → #pred(@y)
#add(#neg(#s(#s(@x))), @y) → #pred(#add(#pos(#s(@x)), @y))
#add(#pos(#s(#0)), @y) → #succ(@y)
#add(#pos(#s(#s(@x))), @y) → #succ(#add(#pos(#s(@x)), @y))
#mult(#0, #0) → #0
#mult(#0, #neg(@y)) → #0
#mult(#0, #pos(@y)) → #0
#mult(#neg(@x), #0) → #0
#mult(#neg(@x), #neg(@y)) → #pos(#natmult(@x, @y))
#mult(#neg(@x), #pos(@y)) → #neg(#natmult(@x, @y))
#mult(#pos(@x), #0) → #0
#mult(#pos(@x), #neg(@y)) → #neg(#natmult(@x, @y))
#mult(#pos(@x), #pos(@y)) → #pos(#natmult(@x, @y))
#natmult(#0, @y) → #0
#natmult(#s(@x), @y) → #add(#pos(@y), #natmult(@x, @y))
#pred(#0) → #neg(#s(#0))
#pred(#neg(#s(@x))) → #neg(#s(#s(@x)))
#pred(#pos(#s(#0))) → #0
#pred(#pos(#s(#s(@x)))) → #pos(#s(@x))
#succ(#0) → #pos(#s(#0))
#succ(#neg(#s(#0))) → #0
#succ(#neg(#s(#s(@x)))) → #neg(#s(@x))
#succ(#pos(#s(@x))) → #pos(#s(#s(@x)))

Types:
#abs :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
#0 :: #0:#neg:#pos:#s::::nil
#neg :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
#pos :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
#s :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
*' :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
#mult :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
+' :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
#add :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
attach :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
attach#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
:: :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
attach#2 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
nil :: #0:#neg:#pos:#s::::nil
lineMult :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
lineMult#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
mult :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
m1 :: #0:#neg:#pos:#s::::nil
m2 :: #0:#neg:#pos:#s::::nil
m3 :: #0:#neg:#pos:#s::::nil
m4 :: #0:#neg:#pos:#s::::nil
makeBase :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
makeBase#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
mkBase :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
matrixMult :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
matrixMult' :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
transAcc :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
matrixMult'#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
matrixMult3 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
matrixMultList :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
matrixMultList#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
matrixMultOld :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
transpose :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
mkBase#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
mult#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
mult#2 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
split :: #0:#neg:#pos:#s::::nil → tuple#2
split#1 :: #0:#neg:#pos:#s::::nil → tuple#2
split#2 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → tuple#2
tuple#2 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → tuple#2
split#3 :: tuple#2 → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → tuple#2
transAcc#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
transpose#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
transpose#2 :: tuple#2 → #0:#neg:#pos:#s::::nil
transpose#3 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
transpose' :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
#pred :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
#succ :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
#natmult :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
hole_#0:#neg:#pos:#s::::nil1_5 :: #0:#neg:#pos:#s::::nil
hole_tuple#22_5 :: tuple#2
gen_#0:#neg:#pos:#s::::nil3_5 :: Nat → #0:#neg:#pos:#s::::nil

Generator Equations:
gen_#0:#neg:#pos:#s::::nil3_5(0) ⇔ #0
gen_#0:#neg:#pos:#s::::nil3_5(+(x, 1)) ⇔ #neg(gen_#0:#neg:#pos:#s::::nil3_5(x))

The following defined symbols remain to be analysed:
transpose#2, attach, attach#1, lineMult, lineMult#1, mult, mkBase, matrixMult', transAcc, matrixMult'#1, matrixMultList, matrixMultList#1, transpose, mkBase#1, mult#1, transAcc#1

They will be analysed ascendingly in the following order:
attach = attach#1
attach < transAcc#1
lineMult = lineMult#1
lineMult < matrixMult'#1
mult < lineMult#1
mult = mult#1
mkBase = mkBase#1
matrixMult' = matrixMult'#1
transAcc = transAcc#1
matrixMultList = matrixMultList#1
transpose = transpose#2

(19) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol transpose#2.

(20) Obligation:

Innermost TRS:
Rules:
#abs(#0) → #0
#abs(#neg(@x)) → #pos(@x)
#abs(#pos(@x)) → #pos(@x)
#abs(#s(@x)) → #pos(#s(@x))
*'(@x, @y) → #mult(@x, @y)
+'(@x, @y) → #add(@x, @y)
attach(@line, @m) → attach#1(@line, @m)
attach#1(::(@x, @xs), @m) → attach#2(@m, @x, @xs)
attach#1(nil, @m) → nil
attach#2(::(@l, @ls), @x, @xs) → ::(::(@x, @l), attach(@xs, @ls))
attach#2(nil, @x, @xs) → nil
lineMult(@l, @m2) → lineMult#1(@m2, @l)
lineMult#1(::(@x, @xs), @l) → ::(mult(@l, @x), lineMult(@l, @xs))
lineMult#1(nil, @l) → nil
m1 → ::(::(#abs(#pos(#s(#0))), ::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#0))))), nil))), ::(::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#0))))), ::(#abs(#pos(#s(#s(#s(#s(#0)))))), nil))), nil))
m2 → ::(::(#abs(#pos(#s(#0))), ::(#abs(#pos(#s(#s(#0)))), nil)), ::(::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#0))))), nil)), ::(::(#abs(#pos(#s(#s(#s(#s(#0)))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#0))))))), nil)), nil)))
m3 → ::(::(#abs(#pos(#s(#0))), ::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#0))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#0))))))), nil)))), ::(::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#0))))), ::(#abs(#pos(#s(#s(#s(#s(#0)))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#0))))))), nil)))), nil))
m4 → ::(::(#abs(#pos(#s(#0))), nil), ::(::(#abs(#pos(#s(#s(#0)))), nil), ::(::(#abs(#pos(#s(#s(#s(#0))))), nil), ::(::(#abs(#pos(#s(#s(#s(#s(#0)))))), nil), nil))))
makeBase(@m) → makeBase#1(@m)
makeBase#1(::(@l, @m')) → mkBase(@l)
makeBase#1(nil) → nil
matrixMult(@m1, @m2) → matrixMult'(@m1, transAcc(@m2, makeBase(@m2)))
matrixMult'(@m1, @m2) → matrixMult'#1(@m1, @m2)
matrixMult'#1(::(@l, @ls), @m2) → ::(lineMult(@l, @m2), matrixMult'(@ls, @m2))
matrixMult'#1(nil, @m2) → nil
matrixMult3(@m1, @m2, @m3) → matrixMult(matrixMult(@m1, @m2), @m3)
matrixMultList(@acc, @mm) → matrixMultList#1(@mm, @acc)
matrixMultList#1(::(@m, @ms), @acc) → matrixMultList(matrixMult(@acc, @m), @ms)
matrixMultList#1(nil, @acc) → @acc
matrixMultOld(@m1, @m2) → matrixMult'(@m1, transpose(@m2))
mkBase(@m) → mkBase#1(@m)
mkBase#1(::(@l, @m')) → ::(nil, mkBase(@m'))
mkBase#1(nil) → nil
mult(@l1, @l2) → mult#1(@l1, @l2)
mult#1(::(@x, @xs), @l2) → mult#2(@l2, @x, @xs)
mult#1(nil, @l2) → #abs(#0)
mult#2(::(@y, @ys), @x, @xs) → +'(*'(@x, @y), mult(@xs, @ys))
mult#2(nil, @x, @xs) → #abs(#0)
split(@m) → split#1(@m)
split#1(::(@l, @ls)) → split#2(@l, @ls)
split#1(nil) → tuple#2(nil, nil)
split#2(::(@x, @xs), @ls) → split#3(split(@ls), @x, @xs)
split#2(nil, @ls) → tuple#2(nil, nil)
split#3(tuple#2(@ys, @m'), @x, @xs) → tuple#2(::(@x, @ys), ::(@xs, @m'))
transAcc(@m, @base) → transAcc#1(@m, @base)
transAcc#1(::(@l, @m'), @base) → attach(@l, transAcc(@m', @base))
transAcc#1(nil, @base) → @base
transpose(@m) → transpose#1(@m, @m)
transpose#1(::(@xs, @xss), @m) → transpose#2(split(@m))
transpose#1(nil, @m) → nil
transpose#2(tuple#2(@l, @m')) → transpose#3(@m', @l)
transpose#3(::(@y, @ys), @l) → ::(@l, transpose(::(@y, @ys)))
transpose#3(nil, @l) → nil
transpose'(@m) → transAcc(@m, makeBase(@m))
#add(#0, @y) → @y
#add(#neg(#s(#0)), @y) → #pred(@y)
#add(#neg(#s(#s(@x))), @y) → #pred(#add(#pos(#s(@x)), @y))
#add(#pos(#s(#0)), @y) → #succ(@y)
#add(#pos(#s(#s(@x))), @y) → #succ(#add(#pos(#s(@x)), @y))
#mult(#0, #0) → #0
#mult(#0, #neg(@y)) → #0
#mult(#0, #pos(@y)) → #0
#mult(#neg(@x), #0) → #0
#mult(#neg(@x), #neg(@y)) → #pos(#natmult(@x, @y))
#mult(#neg(@x), #pos(@y)) → #neg(#natmult(@x, @y))
#mult(#pos(@x), #0) → #0
#mult(#pos(@x), #neg(@y)) → #neg(#natmult(@x, @y))
#mult(#pos(@x), #pos(@y)) → #pos(#natmult(@x, @y))
#natmult(#0, @y) → #0
#natmult(#s(@x), @y) → #add(#pos(@y), #natmult(@x, @y))
#pred(#0) → #neg(#s(#0))
#pred(#neg(#s(@x))) → #neg(#s(#s(@x)))
#pred(#pos(#s(#0))) → #0
#pred(#pos(#s(#s(@x)))) → #pos(#s(@x))
#succ(#0) → #pos(#s(#0))
#succ(#neg(#s(#0))) → #0
#succ(#neg(#s(#s(@x)))) → #neg(#s(@x))
#succ(#pos(#s(@x))) → #pos(#s(#s(@x)))

Types:
#abs :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
#0 :: #0:#neg:#pos:#s::::nil
#neg :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
#pos :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
#s :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
*' :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
#mult :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
+' :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
#add :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
attach :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
attach#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
:: :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
attach#2 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
nil :: #0:#neg:#pos:#s::::nil
lineMult :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
lineMult#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
mult :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
m1 :: #0:#neg:#pos:#s::::nil
m2 :: #0:#neg:#pos:#s::::nil
m3 :: #0:#neg:#pos:#s::::nil
m4 :: #0:#neg:#pos:#s::::nil
makeBase :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
makeBase#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
mkBase :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
matrixMult :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
matrixMult' :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
transAcc :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
matrixMult'#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
matrixMult3 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
matrixMultList :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
matrixMultList#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
matrixMultOld :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
transpose :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
mkBase#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
mult#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
mult#2 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
split :: #0:#neg:#pos:#s::::nil → tuple#2
split#1 :: #0:#neg:#pos:#s::::nil → tuple#2
split#2 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → tuple#2
tuple#2 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → tuple#2
split#3 :: tuple#2 → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → tuple#2
transAcc#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
transpose#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
transpose#2 :: tuple#2 → #0:#neg:#pos:#s::::nil
transpose#3 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
transpose' :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
#pred :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
#succ :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
#natmult :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
hole_#0:#neg:#pos:#s::::nil1_5 :: #0:#neg:#pos:#s::::nil
hole_tuple#22_5 :: tuple#2
gen_#0:#neg:#pos:#s::::nil3_5 :: Nat → #0:#neg:#pos:#s::::nil

Generator Equations:
gen_#0:#neg:#pos:#s::::nil3_5(0) ⇔ #0
gen_#0:#neg:#pos:#s::::nil3_5(+(x, 1)) ⇔ #neg(gen_#0:#neg:#pos:#s::::nil3_5(x))

The following defined symbols remain to be analysed:
transpose, attach, attach#1, lineMult, lineMult#1, mult, mkBase, matrixMult', transAcc, matrixMult'#1, matrixMultList, matrixMultList#1, mkBase#1, mult#1, transAcc#1

They will be analysed ascendingly in the following order:
attach = attach#1
attach < transAcc#1
lineMult = lineMult#1
lineMult < matrixMult'#1
mult < lineMult#1
mult = mult#1
mkBase = mkBase#1
matrixMult' = matrixMult'#1
transAcc = transAcc#1
matrixMultList = matrixMultList#1
transpose = transpose#2

(21) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol transpose.

(22) Obligation:

Innermost TRS:
Rules:
#abs(#0) → #0
#abs(#neg(@x)) → #pos(@x)
#abs(#pos(@x)) → #pos(@x)
#abs(#s(@x)) → #pos(#s(@x))
*'(@x, @y) → #mult(@x, @y)
+'(@x, @y) → #add(@x, @y)
attach(@line, @m) → attach#1(@line, @m)
attach#1(::(@x, @xs), @m) → attach#2(@m, @x, @xs)
attach#1(nil, @m) → nil
attach#2(::(@l, @ls), @x, @xs) → ::(::(@x, @l), attach(@xs, @ls))
attach#2(nil, @x, @xs) → nil
lineMult(@l, @m2) → lineMult#1(@m2, @l)
lineMult#1(::(@x, @xs), @l) → ::(mult(@l, @x), lineMult(@l, @xs))
lineMult#1(nil, @l) → nil
m1 → ::(::(#abs(#pos(#s(#0))), ::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#0))))), nil))), ::(::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#0))))), ::(#abs(#pos(#s(#s(#s(#s(#0)))))), nil))), nil))
m2 → ::(::(#abs(#pos(#s(#0))), ::(#abs(#pos(#s(#s(#0)))), nil)), ::(::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#0))))), nil)), ::(::(#abs(#pos(#s(#s(#s(#s(#0)))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#0))))))), nil)), nil)))
m3 → ::(::(#abs(#pos(#s(#0))), ::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#0))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#0))))))), nil)))), ::(::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#0))))), ::(#abs(#pos(#s(#s(#s(#s(#0)))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#0))))))), nil)))), nil))
m4 → ::(::(#abs(#pos(#s(#0))), nil), ::(::(#abs(#pos(#s(#s(#0)))), nil), ::(::(#abs(#pos(#s(#s(#s(#0))))), nil), ::(::(#abs(#pos(#s(#s(#s(#s(#0)))))), nil), nil))))
makeBase(@m) → makeBase#1(@m)
makeBase#1(::(@l, @m')) → mkBase(@l)
makeBase#1(nil) → nil
matrixMult(@m1, @m2) → matrixMult'(@m1, transAcc(@m2, makeBase(@m2)))
matrixMult'(@m1, @m2) → matrixMult'#1(@m1, @m2)
matrixMult'#1(::(@l, @ls), @m2) → ::(lineMult(@l, @m2), matrixMult'(@ls, @m2))
matrixMult'#1(nil, @m2) → nil
matrixMult3(@m1, @m2, @m3) → matrixMult(matrixMult(@m1, @m2), @m3)
matrixMultList(@acc, @mm) → matrixMultList#1(@mm, @acc)
matrixMultList#1(::(@m, @ms), @acc) → matrixMultList(matrixMult(@acc, @m), @ms)
matrixMultList#1(nil, @acc) → @acc
matrixMultOld(@m1, @m2) → matrixMult'(@m1, transpose(@m2))
mkBase(@m) → mkBase#1(@m)
mkBase#1(::(@l, @m')) → ::(nil, mkBase(@m'))
mkBase#1(nil) → nil
mult(@l1, @l2) → mult#1(@l1, @l2)
mult#1(::(@x, @xs), @l2) → mult#2(@l2, @x, @xs)
mult#1(nil, @l2) → #abs(#0)
mult#2(::(@y, @ys), @x, @xs) → +'(*'(@x, @y), mult(@xs, @ys))
mult#2(nil, @x, @xs) → #abs(#0)
split(@m) → split#1(@m)
split#1(::(@l, @ls)) → split#2(@l, @ls)
split#1(nil) → tuple#2(nil, nil)
split#2(::(@x, @xs), @ls) → split#3(split(@ls), @x, @xs)
split#2(nil, @ls) → tuple#2(nil, nil)
split#3(tuple#2(@ys, @m'), @x, @xs) → tuple#2(::(@x, @ys), ::(@xs, @m'))
transAcc(@m, @base) → transAcc#1(@m, @base)
transAcc#1(::(@l, @m'), @base) → attach(@l, transAcc(@m', @base))
transAcc#1(nil, @base) → @base
transpose(@m) → transpose#1(@m, @m)
transpose#1(::(@xs, @xss), @m) → transpose#2(split(@m))
transpose#1(nil, @m) → nil
transpose#2(tuple#2(@l, @m')) → transpose#3(@m', @l)
transpose#3(::(@y, @ys), @l) → ::(@l, transpose(::(@y, @ys)))
transpose#3(nil, @l) → nil
transpose'(@m) → transAcc(@m, makeBase(@m))
#add(#0, @y) → @y
#add(#neg(#s(#0)), @y) → #pred(@y)
#add(#neg(#s(#s(@x))), @y) → #pred(#add(#pos(#s(@x)), @y))
#add(#pos(#s(#0)), @y) → #succ(@y)
#add(#pos(#s(#s(@x))), @y) → #succ(#add(#pos(#s(@x)), @y))
#mult(#0, #0) → #0
#mult(#0, #neg(@y)) → #0
#mult(#0, #pos(@y)) → #0
#mult(#neg(@x), #0) → #0
#mult(#neg(@x), #neg(@y)) → #pos(#natmult(@x, @y))
#mult(#neg(@x), #pos(@y)) → #neg(#natmult(@x, @y))
#mult(#pos(@x), #0) → #0
#mult(#pos(@x), #neg(@y)) → #neg(#natmult(@x, @y))
#mult(#pos(@x), #pos(@y)) → #pos(#natmult(@x, @y))
#natmult(#0, @y) → #0
#natmult(#s(@x), @y) → #add(#pos(@y), #natmult(@x, @y))
#pred(#0) → #neg(#s(#0))
#pred(#neg(#s(@x))) → #neg(#s(#s(@x)))
#pred(#pos(#s(#0))) → #0
#pred(#pos(#s(#s(@x)))) → #pos(#s(@x))
#succ(#0) → #pos(#s(#0))
#succ(#neg(#s(#0))) → #0
#succ(#neg(#s(#s(@x)))) → #neg(#s(@x))
#succ(#pos(#s(@x))) → #pos(#s(#s(@x)))

Types:
#abs :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
#0 :: #0:#neg:#pos:#s::::nil
#neg :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
#pos :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
#s :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
*' :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
#mult :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
+' :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
#add :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
attach :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
attach#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
:: :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
attach#2 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
nil :: #0:#neg:#pos:#s::::nil
lineMult :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
lineMult#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
mult :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
m1 :: #0:#neg:#pos:#s::::nil
m2 :: #0:#neg:#pos:#s::::nil
m3 :: #0:#neg:#pos:#s::::nil
m4 :: #0:#neg:#pos:#s::::nil
makeBase :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
makeBase#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
mkBase :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
matrixMult :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
matrixMult' :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
transAcc :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
matrixMult'#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
matrixMult3 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
matrixMultList :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
matrixMultList#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
matrixMultOld :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
transpose :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
mkBase#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
mult#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
mult#2 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
split :: #0:#neg:#pos:#s::::nil → tuple#2
split#1 :: #0:#neg:#pos:#s::::nil → tuple#2
split#2 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → tuple#2
tuple#2 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → tuple#2
split#3 :: tuple#2 → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → tuple#2
transAcc#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
transpose#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
transpose#2 :: tuple#2 → #0:#neg:#pos:#s::::nil
transpose#3 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
transpose' :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
#pred :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
#succ :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
#natmult :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
hole_#0:#neg:#pos:#s::::nil1_5 :: #0:#neg:#pos:#s::::nil
hole_tuple#22_5 :: tuple#2
gen_#0:#neg:#pos:#s::::nil3_5 :: Nat → #0:#neg:#pos:#s::::nil

Generator Equations:
gen_#0:#neg:#pos:#s::::nil3_5(0) ⇔ #0
gen_#0:#neg:#pos:#s::::nil3_5(+(x, 1)) ⇔ #neg(gen_#0:#neg:#pos:#s::::nil3_5(x))

The following defined symbols remain to be analysed:
matrixMultList#1, attach, attach#1, lineMult, lineMult#1, mult, mkBase, matrixMult', transAcc, matrixMult'#1, matrixMultList, mkBase#1, mult#1, transAcc#1

They will be analysed ascendingly in the following order:
attach = attach#1
attach < transAcc#1
lineMult = lineMult#1
lineMult < matrixMult'#1
mult < lineMult#1
mult = mult#1
mkBase = mkBase#1
matrixMult' = matrixMult'#1
transAcc = transAcc#1
matrixMultList = matrixMultList#1

(23) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol matrixMultList#1.

(24) Obligation:

Innermost TRS:
Rules:
#abs(#0) → #0
#abs(#neg(@x)) → #pos(@x)
#abs(#pos(@x)) → #pos(@x)
#abs(#s(@x)) → #pos(#s(@x))
*'(@x, @y) → #mult(@x, @y)
+'(@x, @y) → #add(@x, @y)
attach(@line, @m) → attach#1(@line, @m)
attach#1(::(@x, @xs), @m) → attach#2(@m, @x, @xs)
attach#1(nil, @m) → nil
attach#2(::(@l, @ls), @x, @xs) → ::(::(@x, @l), attach(@xs, @ls))
attach#2(nil, @x, @xs) → nil
lineMult(@l, @m2) → lineMult#1(@m2, @l)
lineMult#1(::(@x, @xs), @l) → ::(mult(@l, @x), lineMult(@l, @xs))
lineMult#1(nil, @l) → nil
m1 → ::(::(#abs(#pos(#s(#0))), ::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#0))))), nil))), ::(::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#0))))), ::(#abs(#pos(#s(#s(#s(#s(#0)))))), nil))), nil))
m2 → ::(::(#abs(#pos(#s(#0))), ::(#abs(#pos(#s(#s(#0)))), nil)), ::(::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#0))))), nil)), ::(::(#abs(#pos(#s(#s(#s(#s(#0)))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#0))))))), nil)), nil)))
m3 → ::(::(#abs(#pos(#s(#0))), ::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#0))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#0))))))), nil)))), ::(::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#0))))), ::(#abs(#pos(#s(#s(#s(#s(#0)))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#0))))))), nil)))), nil))
m4 → ::(::(#abs(#pos(#s(#0))), nil), ::(::(#abs(#pos(#s(#s(#0)))), nil), ::(::(#abs(#pos(#s(#s(#s(#0))))), nil), ::(::(#abs(#pos(#s(#s(#s(#s(#0)))))), nil), nil))))
makeBase(@m) → makeBase#1(@m)
makeBase#1(::(@l, @m')) → mkBase(@l)
makeBase#1(nil) → nil
matrixMult(@m1, @m2) → matrixMult'(@m1, transAcc(@m2, makeBase(@m2)))
matrixMult'(@m1, @m2) → matrixMult'#1(@m1, @m2)
matrixMult'#1(::(@l, @ls), @m2) → ::(lineMult(@l, @m2), matrixMult'(@ls, @m2))
matrixMult'#1(nil, @m2) → nil
matrixMult3(@m1, @m2, @m3) → matrixMult(matrixMult(@m1, @m2), @m3)
matrixMultList(@acc, @mm) → matrixMultList#1(@mm, @acc)
matrixMultList#1(::(@m, @ms), @acc) → matrixMultList(matrixMult(@acc, @m), @ms)
matrixMultList#1(nil, @acc) → @acc
matrixMultOld(@m1, @m2) → matrixMult'(@m1, transpose(@m2))
mkBase(@m) → mkBase#1(@m)
mkBase#1(::(@l, @m')) → ::(nil, mkBase(@m'))
mkBase#1(nil) → nil
mult(@l1, @l2) → mult#1(@l1, @l2)
mult#1(::(@x, @xs), @l2) → mult#2(@l2, @x, @xs)
mult#1(nil, @l2) → #abs(#0)
mult#2(::(@y, @ys), @x, @xs) → +'(*'(@x, @y), mult(@xs, @ys))
mult#2(nil, @x, @xs) → #abs(#0)
split(@m) → split#1(@m)
split#1(::(@l, @ls)) → split#2(@l, @ls)
split#1(nil) → tuple#2(nil, nil)
split#2(::(@x, @xs), @ls) → split#3(split(@ls), @x, @xs)
split#2(nil, @ls) → tuple#2(nil, nil)
split#3(tuple#2(@ys, @m'), @x, @xs) → tuple#2(::(@x, @ys), ::(@xs, @m'))
transAcc(@m, @base) → transAcc#1(@m, @base)
transAcc#1(::(@l, @m'), @base) → attach(@l, transAcc(@m', @base))
transAcc#1(nil, @base) → @base
transpose(@m) → transpose#1(@m, @m)
transpose#1(::(@xs, @xss), @m) → transpose#2(split(@m))
transpose#1(nil, @m) → nil
transpose#2(tuple#2(@l, @m')) → transpose#3(@m', @l)
transpose#3(::(@y, @ys), @l) → ::(@l, transpose(::(@y, @ys)))
transpose#3(nil, @l) → nil
transpose'(@m) → transAcc(@m, makeBase(@m))
#add(#0, @y) → @y
#add(#neg(#s(#0)), @y) → #pred(@y)
#add(#neg(#s(#s(@x))), @y) → #pred(#add(#pos(#s(@x)), @y))
#add(#pos(#s(#0)), @y) → #succ(@y)
#add(#pos(#s(#s(@x))), @y) → #succ(#add(#pos(#s(@x)), @y))
#mult(#0, #0) → #0
#mult(#0, #neg(@y)) → #0
#mult(#0, #pos(@y)) → #0
#mult(#neg(@x), #0) → #0
#mult(#neg(@x), #neg(@y)) → #pos(#natmult(@x, @y))
#mult(#neg(@x), #pos(@y)) → #neg(#natmult(@x, @y))
#mult(#pos(@x), #0) → #0
#mult(#pos(@x), #neg(@y)) → #neg(#natmult(@x, @y))
#mult(#pos(@x), #pos(@y)) → #pos(#natmult(@x, @y))
#natmult(#0, @y) → #0
#natmult(#s(@x), @y) → #add(#pos(@y), #natmult(@x, @y))
#pred(#0) → #neg(#s(#0))
#pred(#neg(#s(@x))) → #neg(#s(#s(@x)))
#pred(#pos(#s(#0))) → #0
#pred(#pos(#s(#s(@x)))) → #pos(#s(@x))
#succ(#0) → #pos(#s(#0))
#succ(#neg(#s(#0))) → #0
#succ(#neg(#s(#s(@x)))) → #neg(#s(@x))
#succ(#pos(#s(@x))) → #pos(#s(#s(@x)))

Types:
#abs :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
#0 :: #0:#neg:#pos:#s::::nil
#neg :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
#pos :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
#s :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
*' :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
#mult :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
+' :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
#add :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
attach :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
attach#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
:: :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
attach#2 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
nil :: #0:#neg:#pos:#s::::nil
lineMult :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
lineMult#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
mult :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
m1 :: #0:#neg:#pos:#s::::nil
m2 :: #0:#neg:#pos:#s::::nil
m3 :: #0:#neg:#pos:#s::::nil
m4 :: #0:#neg:#pos:#s::::nil
makeBase :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
makeBase#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
mkBase :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
matrixMult :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
matrixMult' :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
transAcc :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
matrixMult'#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
matrixMult3 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
matrixMultList :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
matrixMultList#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
matrixMultOld :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
transpose :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
mkBase#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
mult#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
mult#2 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
split :: #0:#neg:#pos:#s::::nil → tuple#2
split#1 :: #0:#neg:#pos:#s::::nil → tuple#2
split#2 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → tuple#2
tuple#2 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → tuple#2
split#3 :: tuple#2 → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → tuple#2
transAcc#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
transpose#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
transpose#2 :: tuple#2 → #0:#neg:#pos:#s::::nil
transpose#3 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
transpose' :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
#pred :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
#succ :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
#natmult :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
hole_#0:#neg:#pos:#s::::nil1_5 :: #0:#neg:#pos:#s::::nil
hole_tuple#22_5 :: tuple#2
gen_#0:#neg:#pos:#s::::nil3_5 :: Nat → #0:#neg:#pos:#s::::nil

Generator Equations:
gen_#0:#neg:#pos:#s::::nil3_5(0) ⇔ #0
gen_#0:#neg:#pos:#s::::nil3_5(+(x, 1)) ⇔ #neg(gen_#0:#neg:#pos:#s::::nil3_5(x))

The following defined symbols remain to be analysed:
matrixMultList, attach, attach#1, lineMult, lineMult#1, mult, mkBase, matrixMult', transAcc, matrixMult'#1, mkBase#1, mult#1, transAcc#1

They will be analysed ascendingly in the following order:
attach = attach#1
attach < transAcc#1
lineMult = lineMult#1
lineMult < matrixMult'#1
mult < lineMult#1
mult = mult#1
mkBase = mkBase#1
matrixMult' = matrixMult'#1
transAcc = transAcc#1
matrixMultList = matrixMultList#1

(25) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol matrixMultList.

(26) Obligation:

Innermost TRS:
Rules:
#abs(#0) → #0
#abs(#neg(@x)) → #pos(@x)
#abs(#pos(@x)) → #pos(@x)
#abs(#s(@x)) → #pos(#s(@x))
*'(@x, @y) → #mult(@x, @y)
+'(@x, @y) → #add(@x, @y)
attach(@line, @m) → attach#1(@line, @m)
attach#1(::(@x, @xs), @m) → attach#2(@m, @x, @xs)
attach#1(nil, @m) → nil
attach#2(::(@l, @ls), @x, @xs) → ::(::(@x, @l), attach(@xs, @ls))
attach#2(nil, @x, @xs) → nil
lineMult(@l, @m2) → lineMult#1(@m2, @l)
lineMult#1(::(@x, @xs), @l) → ::(mult(@l, @x), lineMult(@l, @xs))
lineMult#1(nil, @l) → nil
m1 → ::(::(#abs(#pos(#s(#0))), ::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#0))))), nil))), ::(::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#0))))), ::(#abs(#pos(#s(#s(#s(#s(#0)))))), nil))), nil))
m2 → ::(::(#abs(#pos(#s(#0))), ::(#abs(#pos(#s(#s(#0)))), nil)), ::(::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#0))))), nil)), ::(::(#abs(#pos(#s(#s(#s(#s(#0)))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#0))))))), nil)), nil)))
m3 → ::(::(#abs(#pos(#s(#0))), ::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#0))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#0))))))), nil)))), ::(::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#0))))), ::(#abs(#pos(#s(#s(#s(#s(#0)))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#0))))))), nil)))), nil))
m4 → ::(::(#abs(#pos(#s(#0))), nil), ::(::(#abs(#pos(#s(#s(#0)))), nil), ::(::(#abs(#pos(#s(#s(#s(#0))))), nil), ::(::(#abs(#pos(#s(#s(#s(#s(#0)))))), nil), nil))))
makeBase(@m) → makeBase#1(@m)
makeBase#1(::(@l, @m')) → mkBase(@l)
makeBase#1(nil) → nil
matrixMult(@m1, @m2) → matrixMult'(@m1, transAcc(@m2, makeBase(@m2)))
matrixMult'(@m1, @m2) → matrixMult'#1(@m1, @m2)
matrixMult'#1(::(@l, @ls), @m2) → ::(lineMult(@l, @m2), matrixMult'(@ls, @m2))
matrixMult'#1(nil, @m2) → nil
matrixMult3(@m1, @m2, @m3) → matrixMult(matrixMult(@m1, @m2), @m3)
matrixMultList(@acc, @mm) → matrixMultList#1(@mm, @acc)
matrixMultList#1(::(@m, @ms), @acc) → matrixMultList(matrixMult(@acc, @m), @ms)
matrixMultList#1(nil, @acc) → @acc
matrixMultOld(@m1, @m2) → matrixMult'(@m1, transpose(@m2))
mkBase(@m) → mkBase#1(@m)
mkBase#1(::(@l, @m')) → ::(nil, mkBase(@m'))
mkBase#1(nil) → nil
mult(@l1, @l2) → mult#1(@l1, @l2)
mult#1(::(@x, @xs), @l2) → mult#2(@l2, @x, @xs)
mult#1(nil, @l2) → #abs(#0)
mult#2(::(@y, @ys), @x, @xs) → +'(*'(@x, @y), mult(@xs, @ys))
mult#2(nil, @x, @xs) → #abs(#0)
split(@m) → split#1(@m)
split#1(::(@l, @ls)) → split#2(@l, @ls)
split#1(nil) → tuple#2(nil, nil)
split#2(::(@x, @xs), @ls) → split#3(split(@ls), @x, @xs)
split#2(nil, @ls) → tuple#2(nil, nil)
split#3(tuple#2(@ys, @m'), @x, @xs) → tuple#2(::(@x, @ys), ::(@xs, @m'))
transAcc(@m, @base) → transAcc#1(@m, @base)
transAcc#1(::(@l, @m'), @base) → attach(@l, transAcc(@m', @base))
transAcc#1(nil, @base) → @base
transpose(@m) → transpose#1(@m, @m)
transpose#1(::(@xs, @xss), @m) → transpose#2(split(@m))
transpose#1(nil, @m) → nil
transpose#2(tuple#2(@l, @m')) → transpose#3(@m', @l)
transpose#3(::(@y, @ys), @l) → ::(@l, transpose(::(@y, @ys)))
transpose#3(nil, @l) → nil
transpose'(@m) → transAcc(@m, makeBase(@m))
#add(#0, @y) → @y
#add(#neg(#s(#0)), @y) → #pred(@y)
#add(#neg(#s(#s(@x))), @y) → #pred(#add(#pos(#s(@x)), @y))
#add(#pos(#s(#0)), @y) → #succ(@y)
#add(#pos(#s(#s(@x))), @y) → #succ(#add(#pos(#s(@x)), @y))
#mult(#0, #0) → #0
#mult(#0, #neg(@y)) → #0
#mult(#0, #pos(@y)) → #0
#mult(#neg(@x), #0) → #0
#mult(#neg(@x), #neg(@y)) → #pos(#natmult(@x, @y))
#mult(#neg(@x), #pos(@y)) → #neg(#natmult(@x, @y))
#mult(#pos(@x), #0) → #0
#mult(#pos(@x), #neg(@y)) → #neg(#natmult(@x, @y))
#mult(#pos(@x), #pos(@y)) → #pos(#natmult(@x, @y))
#natmult(#0, @y) → #0
#natmult(#s(@x), @y) → #add(#pos(@y), #natmult(@x, @y))
#pred(#0) → #neg(#s(#0))
#pred(#neg(#s(@x))) → #neg(#s(#s(@x)))
#pred(#pos(#s(#0))) → #0
#pred(#pos(#s(#s(@x)))) → #pos(#s(@x))
#succ(#0) → #pos(#s(#0))
#succ(#neg(#s(#0))) → #0
#succ(#neg(#s(#s(@x)))) → #neg(#s(@x))
#succ(#pos(#s(@x))) → #pos(#s(#s(@x)))

Types:
#abs :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
#0 :: #0:#neg:#pos:#s::::nil
#neg :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
#pos :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
#s :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
*' :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
#mult :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
+' :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
#add :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
attach :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
attach#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
:: :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
attach#2 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
nil :: #0:#neg:#pos:#s::::nil
lineMult :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
lineMult#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
mult :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
m1 :: #0:#neg:#pos:#s::::nil
m2 :: #0:#neg:#pos:#s::::nil
m3 :: #0:#neg:#pos:#s::::nil
m4 :: #0:#neg:#pos:#s::::nil
makeBase :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
makeBase#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
mkBase :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
matrixMult :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
matrixMult' :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
transAcc :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
matrixMult'#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
matrixMult3 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
matrixMultList :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
matrixMultList#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
matrixMultOld :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
transpose :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
mkBase#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
mult#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
mult#2 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
split :: #0:#neg:#pos:#s::::nil → tuple#2
split#1 :: #0:#neg:#pos:#s::::nil → tuple#2
split#2 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → tuple#2
tuple#2 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → tuple#2
split#3 :: tuple#2 → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → tuple#2
transAcc#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
transpose#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
transpose#2 :: tuple#2 → #0:#neg:#pos:#s::::nil
transpose#3 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
transpose' :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
#pred :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
#succ :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
#natmult :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
hole_#0:#neg:#pos:#s::::nil1_5 :: #0:#neg:#pos:#s::::nil
hole_tuple#22_5 :: tuple#2
gen_#0:#neg:#pos:#s::::nil3_5 :: Nat → #0:#neg:#pos:#s::::nil

Generator Equations:
gen_#0:#neg:#pos:#s::::nil3_5(0) ⇔ #0
gen_#0:#neg:#pos:#s::::nil3_5(+(x, 1)) ⇔ #neg(gen_#0:#neg:#pos:#s::::nil3_5(x))

The following defined symbols remain to be analysed:
mkBase#1, attach, attach#1, lineMult, lineMult#1, mult, mkBase, matrixMult', transAcc, matrixMult'#1, mult#1, transAcc#1

They will be analysed ascendingly in the following order:
attach = attach#1
attach < transAcc#1
lineMult = lineMult#1
lineMult < matrixMult'#1
mult < lineMult#1
mult = mult#1
mkBase = mkBase#1
matrixMult' = matrixMult'#1
transAcc = transAcc#1

(27) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol mkBase#1.

(28) Obligation:

Innermost TRS:
Rules:
#abs(#0) → #0
#abs(#neg(@x)) → #pos(@x)
#abs(#pos(@x)) → #pos(@x)
#abs(#s(@x)) → #pos(#s(@x))
*'(@x, @y) → #mult(@x, @y)
+'(@x, @y) → #add(@x, @y)
attach(@line, @m) → attach#1(@line, @m)
attach#1(::(@x, @xs), @m) → attach#2(@m, @x, @xs)
attach#1(nil, @m) → nil
attach#2(::(@l, @ls), @x, @xs) → ::(::(@x, @l), attach(@xs, @ls))
attach#2(nil, @x, @xs) → nil
lineMult(@l, @m2) → lineMult#1(@m2, @l)
lineMult#1(::(@x, @xs), @l) → ::(mult(@l, @x), lineMult(@l, @xs))
lineMult#1(nil, @l) → nil
m1 → ::(::(#abs(#pos(#s(#0))), ::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#0))))), nil))), ::(::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#0))))), ::(#abs(#pos(#s(#s(#s(#s(#0)))))), nil))), nil))
m2 → ::(::(#abs(#pos(#s(#0))), ::(#abs(#pos(#s(#s(#0)))), nil)), ::(::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#0))))), nil)), ::(::(#abs(#pos(#s(#s(#s(#s(#0)))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#0))))))), nil)), nil)))
m3 → ::(::(#abs(#pos(#s(#0))), ::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#0))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#0))))))), nil)))), ::(::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#0))))), ::(#abs(#pos(#s(#s(#s(#s(#0)))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#0))))))), nil)))), nil))
m4 → ::(::(#abs(#pos(#s(#0))), nil), ::(::(#abs(#pos(#s(#s(#0)))), nil), ::(::(#abs(#pos(#s(#s(#s(#0))))), nil), ::(::(#abs(#pos(#s(#s(#s(#s(#0)))))), nil), nil))))
makeBase(@m) → makeBase#1(@m)
makeBase#1(::(@l, @m')) → mkBase(@l)
makeBase#1(nil) → nil
matrixMult(@m1, @m2) → matrixMult'(@m1, transAcc(@m2, makeBase(@m2)))
matrixMult'(@m1, @m2) → matrixMult'#1(@m1, @m2)
matrixMult'#1(::(@l, @ls), @m2) → ::(lineMult(@l, @m2), matrixMult'(@ls, @m2))
matrixMult'#1(nil, @m2) → nil
matrixMult3(@m1, @m2, @m3) → matrixMult(matrixMult(@m1, @m2), @m3)
matrixMultList(@acc, @mm) → matrixMultList#1(@mm, @acc)
matrixMultList#1(::(@m, @ms), @acc) → matrixMultList(matrixMult(@acc, @m), @ms)
matrixMultList#1(nil, @acc) → @acc
matrixMultOld(@m1, @m2) → matrixMult'(@m1, transpose(@m2))
mkBase(@m) → mkBase#1(@m)
mkBase#1(::(@l, @m')) → ::(nil, mkBase(@m'))
mkBase#1(nil) → nil
mult(@l1, @l2) → mult#1(@l1, @l2)
mult#1(::(@x, @xs), @l2) → mult#2(@l2, @x, @xs)
mult#1(nil, @l2) → #abs(#0)
mult#2(::(@y, @ys), @x, @xs) → +'(*'(@x, @y), mult(@xs, @ys))
mult#2(nil, @x, @xs) → #abs(#0)
split(@m) → split#1(@m)
split#1(::(@l, @ls)) → split#2(@l, @ls)
split#1(nil) → tuple#2(nil, nil)
split#2(::(@x, @xs), @ls) → split#3(split(@ls), @x, @xs)
split#2(nil, @ls) → tuple#2(nil, nil)
split#3(tuple#2(@ys, @m'), @x, @xs) → tuple#2(::(@x, @ys), ::(@xs, @m'))
transAcc(@m, @base) → transAcc#1(@m, @base)
transAcc#1(::(@l, @m'), @base) → attach(@l, transAcc(@m', @base))
transAcc#1(nil, @base) → @base
transpose(@m) → transpose#1(@m, @m)
transpose#1(::(@xs, @xss), @m) → transpose#2(split(@m))
transpose#1(nil, @m) → nil
transpose#2(tuple#2(@l, @m')) → transpose#3(@m', @l)
transpose#3(::(@y, @ys), @l) → ::(@l, transpose(::(@y, @ys)))
transpose#3(nil, @l) → nil
transpose'(@m) → transAcc(@m, makeBase(@m))
#add(#0, @y) → @y
#add(#neg(#s(#0)), @y) → #pred(@y)
#add(#neg(#s(#s(@x))), @y) → #pred(#add(#pos(#s(@x)), @y))
#add(#pos(#s(#0)), @y) → #succ(@y)
#add(#pos(#s(#s(@x))), @y) → #succ(#add(#pos(#s(@x)), @y))
#mult(#0, #0) → #0
#mult(#0, #neg(@y)) → #0
#mult(#0, #pos(@y)) → #0
#mult(#neg(@x), #0) → #0
#mult(#neg(@x), #neg(@y)) → #pos(#natmult(@x, @y))
#mult(#neg(@x), #pos(@y)) → #neg(#natmult(@x, @y))
#mult(#pos(@x), #0) → #0
#mult(#pos(@x), #neg(@y)) → #neg(#natmult(@x, @y))
#mult(#pos(@x), #pos(@y)) → #pos(#natmult(@x, @y))
#natmult(#0, @y) → #0
#natmult(#s(@x), @y) → #add(#pos(@y), #natmult(@x, @y))
#pred(#0) → #neg(#s(#0))
#pred(#neg(#s(@x))) → #neg(#s(#s(@x)))
#pred(#pos(#s(#0))) → #0
#pred(#pos(#s(#s(@x)))) → #pos(#s(@x))
#succ(#0) → #pos(#s(#0))
#succ(#neg(#s(#0))) → #0
#succ(#neg(#s(#s(@x)))) → #neg(#s(@x))
#succ(#pos(#s(@x))) → #pos(#s(#s(@x)))

Types:
#abs :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
#0 :: #0:#neg:#pos:#s::::nil
#neg :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
#pos :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
#s :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
*' :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
#mult :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
+' :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
#add :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
attach :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
attach#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
:: :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
attach#2 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
nil :: #0:#neg:#pos:#s::::nil
lineMult :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
lineMult#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
mult :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
m1 :: #0:#neg:#pos:#s::::nil
m2 :: #0:#neg:#pos:#s::::nil
m3 :: #0:#neg:#pos:#s::::nil
m4 :: #0:#neg:#pos:#s::::nil
makeBase :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
makeBase#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
mkBase :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
matrixMult :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
matrixMult' :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
transAcc :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
matrixMult'#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
matrixMult3 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
matrixMultList :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
matrixMultList#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
matrixMultOld :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
transpose :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
mkBase#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
mult#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
mult#2 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
split :: #0:#neg:#pos:#s::::nil → tuple#2
split#1 :: #0:#neg:#pos:#s::::nil → tuple#2
split#2 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → tuple#2
tuple#2 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → tuple#2
split#3 :: tuple#2 → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → tuple#2
transAcc#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
transpose#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
transpose#2 :: tuple#2 → #0:#neg:#pos:#s::::nil
transpose#3 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
transpose' :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
#pred :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
#succ :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
#natmult :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
hole_#0:#neg:#pos:#s::::nil1_5 :: #0:#neg:#pos:#s::::nil
hole_tuple#22_5 :: tuple#2
gen_#0:#neg:#pos:#s::::nil3_5 :: Nat → #0:#neg:#pos:#s::::nil

Generator Equations:
gen_#0:#neg:#pos:#s::::nil3_5(0) ⇔ #0
gen_#0:#neg:#pos:#s::::nil3_5(+(x, 1)) ⇔ #neg(gen_#0:#neg:#pos:#s::::nil3_5(x))

The following defined symbols remain to be analysed:
mkBase, attach, attach#1, lineMult, lineMult#1, mult, matrixMult', transAcc, matrixMult'#1, mult#1, transAcc#1

They will be analysed ascendingly in the following order:
attach = attach#1
attach < transAcc#1
lineMult = lineMult#1
lineMult < matrixMult'#1
mult < lineMult#1
mult = mult#1
mkBase = mkBase#1
matrixMult' = matrixMult'#1
transAcc = transAcc#1

(29) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol mkBase.

(30) Obligation:

Innermost TRS:
Rules:
#abs(#0) → #0
#abs(#neg(@x)) → #pos(@x)
#abs(#pos(@x)) → #pos(@x)
#abs(#s(@x)) → #pos(#s(@x))
*'(@x, @y) → #mult(@x, @y)
+'(@x, @y) → #add(@x, @y)
attach(@line, @m) → attach#1(@line, @m)
attach#1(::(@x, @xs), @m) → attach#2(@m, @x, @xs)
attach#1(nil, @m) → nil
attach#2(::(@l, @ls), @x, @xs) → ::(::(@x, @l), attach(@xs, @ls))
attach#2(nil, @x, @xs) → nil
lineMult(@l, @m2) → lineMult#1(@m2, @l)
lineMult#1(::(@x, @xs), @l) → ::(mult(@l, @x), lineMult(@l, @xs))
lineMult#1(nil, @l) → nil
m1 → ::(::(#abs(#pos(#s(#0))), ::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#0))))), nil))), ::(::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#0))))), ::(#abs(#pos(#s(#s(#s(#s(#0)))))), nil))), nil))
m2 → ::(::(#abs(#pos(#s(#0))), ::(#abs(#pos(#s(#s(#0)))), nil)), ::(::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#0))))), nil)), ::(::(#abs(#pos(#s(#s(#s(#s(#0)))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#0))))))), nil)), nil)))
m3 → ::(::(#abs(#pos(#s(#0))), ::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#0))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#0))))))), nil)))), ::(::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#0))))), ::(#abs(#pos(#s(#s(#s(#s(#0)))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#0))))))), nil)))), nil))
m4 → ::(::(#abs(#pos(#s(#0))), nil), ::(::(#abs(#pos(#s(#s(#0)))), nil), ::(::(#abs(#pos(#s(#s(#s(#0))))), nil), ::(::(#abs(#pos(#s(#s(#s(#s(#0)))))), nil), nil))))
makeBase(@m) → makeBase#1(@m)
makeBase#1(::(@l, @m')) → mkBase(@l)
makeBase#1(nil) → nil
matrixMult(@m1, @m2) → matrixMult'(@m1, transAcc(@m2, makeBase(@m2)))
matrixMult'(@m1, @m2) → matrixMult'#1(@m1, @m2)
matrixMult'#1(::(@l, @ls), @m2) → ::(lineMult(@l, @m2), matrixMult'(@ls, @m2))
matrixMult'#1(nil, @m2) → nil
matrixMult3(@m1, @m2, @m3) → matrixMult(matrixMult(@m1, @m2), @m3)
matrixMultList(@acc, @mm) → matrixMultList#1(@mm, @acc)
matrixMultList#1(::(@m, @ms), @acc) → matrixMultList(matrixMult(@acc, @m), @ms)
matrixMultList#1(nil, @acc) → @acc
matrixMultOld(@m1, @m2) → matrixMult'(@m1, transpose(@m2))
mkBase(@m) → mkBase#1(@m)
mkBase#1(::(@l, @m')) → ::(nil, mkBase(@m'))
mkBase#1(nil) → nil
mult(@l1, @l2) → mult#1(@l1, @l2)
mult#1(::(@x, @xs), @l2) → mult#2(@l2, @x, @xs)
mult#1(nil, @l2) → #abs(#0)
mult#2(::(@y, @ys), @x, @xs) → +'(*'(@x, @y), mult(@xs, @ys))
mult#2(nil, @x, @xs) → #abs(#0)
split(@m) → split#1(@m)
split#1(::(@l, @ls)) → split#2(@l, @ls)
split#1(nil) → tuple#2(nil, nil)
split#2(::(@x, @xs), @ls) → split#3(split(@ls), @x, @xs)
split#2(nil, @ls) → tuple#2(nil, nil)
split#3(tuple#2(@ys, @m'), @x, @xs) → tuple#2(::(@x, @ys), ::(@xs, @m'))
transAcc(@m, @base) → transAcc#1(@m, @base)
transAcc#1(::(@l, @m'), @base) → attach(@l, transAcc(@m', @base))
transAcc#1(nil, @base) → @base
transpose(@m) → transpose#1(@m, @m)
transpose#1(::(@xs, @xss), @m) → transpose#2(split(@m))
transpose#1(nil, @m) → nil
transpose#2(tuple#2(@l, @m')) → transpose#3(@m', @l)
transpose#3(::(@y, @ys), @l) → ::(@l, transpose(::(@y, @ys)))
transpose#3(nil, @l) → nil
transpose'(@m) → transAcc(@m, makeBase(@m))
#add(#0, @y) → @y
#add(#neg(#s(#0)), @y) → #pred(@y)
#add(#neg(#s(#s(@x))), @y) → #pred(#add(#pos(#s(@x)), @y))
#add(#pos(#s(#0)), @y) → #succ(@y)
#add(#pos(#s(#s(@x))), @y) → #succ(#add(#pos(#s(@x)), @y))
#mult(#0, #0) → #0
#mult(#0, #neg(@y)) → #0
#mult(#0, #pos(@y)) → #0
#mult(#neg(@x), #0) → #0
#mult(#neg(@x), #neg(@y)) → #pos(#natmult(@x, @y))
#mult(#neg(@x), #pos(@y)) → #neg(#natmult(@x, @y))
#mult(#pos(@x), #0) → #0
#mult(#pos(@x), #neg(@y)) → #neg(#natmult(@x, @y))
#mult(#pos(@x), #pos(@y)) → #pos(#natmult(@x, @y))
#natmult(#0, @y) → #0
#natmult(#s(@x), @y) → #add(#pos(@y), #natmult(@x, @y))
#pred(#0) → #neg(#s(#0))
#pred(#neg(#s(@x))) → #neg(#s(#s(@x)))
#pred(#pos(#s(#0))) → #0
#pred(#pos(#s(#s(@x)))) → #pos(#s(@x))
#succ(#0) → #pos(#s(#0))
#succ(#neg(#s(#0))) → #0
#succ(#neg(#s(#s(@x)))) → #neg(#s(@x))
#succ(#pos(#s(@x))) → #pos(#s(#s(@x)))

Types:
#abs :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
#0 :: #0:#neg:#pos:#s::::nil
#neg :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
#pos :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
#s :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
*' :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
#mult :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
+' :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
#add :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
attach :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
attach#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
:: :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
attach#2 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
nil :: #0:#neg:#pos:#s::::nil
lineMult :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
lineMult#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
mult :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
m1 :: #0:#neg:#pos:#s::::nil
m2 :: #0:#neg:#pos:#s::::nil
m3 :: #0:#neg:#pos:#s::::nil
m4 :: #0:#neg:#pos:#s::::nil
makeBase :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
makeBase#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
mkBase :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
matrixMult :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
matrixMult' :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
transAcc :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
matrixMult'#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
matrixMult3 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
matrixMultList :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
matrixMultList#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
matrixMultOld :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
transpose :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
mkBase#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
mult#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
mult#2 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
split :: #0:#neg:#pos:#s::::nil → tuple#2
split#1 :: #0:#neg:#pos:#s::::nil → tuple#2
split#2 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → tuple#2
tuple#2 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → tuple#2
split#3 :: tuple#2 → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → tuple#2
transAcc#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
transpose#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
transpose#2 :: tuple#2 → #0:#neg:#pos:#s::::nil
transpose#3 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
transpose' :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
#pred :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
#succ :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
#natmult :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
hole_#0:#neg:#pos:#s::::nil1_5 :: #0:#neg:#pos:#s::::nil
hole_tuple#22_5 :: tuple#2
gen_#0:#neg:#pos:#s::::nil3_5 :: Nat → #0:#neg:#pos:#s::::nil

Generator Equations:
gen_#0:#neg:#pos:#s::::nil3_5(0) ⇔ #0
gen_#0:#neg:#pos:#s::::nil3_5(+(x, 1)) ⇔ #neg(gen_#0:#neg:#pos:#s::::nil3_5(x))

The following defined symbols remain to be analysed:
mult#1, attach, attach#1, lineMult, lineMult#1, mult, matrixMult', transAcc, matrixMult'#1, transAcc#1

They will be analysed ascendingly in the following order:
attach = attach#1
attach < transAcc#1
lineMult = lineMult#1
lineMult < matrixMult'#1
mult < lineMult#1
mult = mult#1
matrixMult' = matrixMult'#1
transAcc = transAcc#1

(31) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol mult#1.

(32) Obligation:

Innermost TRS:
Rules:
#abs(#0) → #0
#abs(#neg(@x)) → #pos(@x)
#abs(#pos(@x)) → #pos(@x)
#abs(#s(@x)) → #pos(#s(@x))
*'(@x, @y) → #mult(@x, @y)
+'(@x, @y) → #add(@x, @y)
attach(@line, @m) → attach#1(@line, @m)
attach#1(::(@x, @xs), @m) → attach#2(@m, @x, @xs)
attach#1(nil, @m) → nil
attach#2(::(@l, @ls), @x, @xs) → ::(::(@x, @l), attach(@xs, @ls))
attach#2(nil, @x, @xs) → nil
lineMult(@l, @m2) → lineMult#1(@m2, @l)
lineMult#1(::(@x, @xs), @l) → ::(mult(@l, @x), lineMult(@l, @xs))
lineMult#1(nil, @l) → nil
m1 → ::(::(#abs(#pos(#s(#0))), ::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#0))))), nil))), ::(::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#0))))), ::(#abs(#pos(#s(#s(#s(#s(#0)))))), nil))), nil))
m2 → ::(::(#abs(#pos(#s(#0))), ::(#abs(#pos(#s(#s(#0)))), nil)), ::(::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#0))))), nil)), ::(::(#abs(#pos(#s(#s(#s(#s(#0)))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#0))))))), nil)), nil)))
m3 → ::(::(#abs(#pos(#s(#0))), ::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#0))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#0))))))), nil)))), ::(::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#0))))), ::(#abs(#pos(#s(#s(#s(#s(#0)))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#0))))))), nil)))), nil))
m4 → ::(::(#abs(#pos(#s(#0))), nil), ::(::(#abs(#pos(#s(#s(#0)))), nil), ::(::(#abs(#pos(#s(#s(#s(#0))))), nil), ::(::(#abs(#pos(#s(#s(#s(#s(#0)))))), nil), nil))))
makeBase(@m) → makeBase#1(@m)
makeBase#1(::(@l, @m')) → mkBase(@l)
makeBase#1(nil) → nil
matrixMult(@m1, @m2) → matrixMult'(@m1, transAcc(@m2, makeBase(@m2)))
matrixMult'(@m1, @m2) → matrixMult'#1(@m1, @m2)
matrixMult'#1(::(@l, @ls), @m2) → ::(lineMult(@l, @m2), matrixMult'(@ls, @m2))
matrixMult'#1(nil, @m2) → nil
matrixMult3(@m1, @m2, @m3) → matrixMult(matrixMult(@m1, @m2), @m3)
matrixMultList(@acc, @mm) → matrixMultList#1(@mm, @acc)
matrixMultList#1(::(@m, @ms), @acc) → matrixMultList(matrixMult(@acc, @m), @ms)
matrixMultList#1(nil, @acc) → @acc
matrixMultOld(@m1, @m2) → matrixMult'(@m1, transpose(@m2))
mkBase(@m) → mkBase#1(@m)
mkBase#1(::(@l, @m')) → ::(nil, mkBase(@m'))
mkBase#1(nil) → nil
mult(@l1, @l2) → mult#1(@l1, @l2)
mult#1(::(@x, @xs), @l2) → mult#2(@l2, @x, @xs)
mult#1(nil, @l2) → #abs(#0)
mult#2(::(@y, @ys), @x, @xs) → +'(*'(@x, @y), mult(@xs, @ys))
mult#2(nil, @x, @xs) → #abs(#0)
split(@m) → split#1(@m)
split#1(::(@l, @ls)) → split#2(@l, @ls)
split#1(nil) → tuple#2(nil, nil)
split#2(::(@x, @xs), @ls) → split#3(split(@ls), @x, @xs)
split#2(nil, @ls) → tuple#2(nil, nil)
split#3(tuple#2(@ys, @m'), @x, @xs) → tuple#2(::(@x, @ys), ::(@xs, @m'))
transAcc(@m, @base) → transAcc#1(@m, @base)
transAcc#1(::(@l, @m'), @base) → attach(@l, transAcc(@m', @base))
transAcc#1(nil, @base) → @base
transpose(@m) → transpose#1(@m, @m)
transpose#1(::(@xs, @xss), @m) → transpose#2(split(@m))
transpose#1(nil, @m) → nil
transpose#2(tuple#2(@l, @m')) → transpose#3(@m', @l)
transpose#3(::(@y, @ys), @l) → ::(@l, transpose(::(@y, @ys)))
transpose#3(nil, @l) → nil
transpose'(@m) → transAcc(@m, makeBase(@m))
#add(#0, @y) → @y
#add(#neg(#s(#0)), @y) → #pred(@y)
#add(#neg(#s(#s(@x))), @y) → #pred(#add(#pos(#s(@x)), @y))
#add(#pos(#s(#0)), @y) → #succ(@y)
#add(#pos(#s(#s(@x))), @y) → #succ(#add(#pos(#s(@x)), @y))
#mult(#0, #0) → #0
#mult(#0, #neg(@y)) → #0
#mult(#0, #pos(@y)) → #0
#mult(#neg(@x), #0) → #0
#mult(#neg(@x), #neg(@y)) → #pos(#natmult(@x, @y))
#mult(#neg(@x), #pos(@y)) → #neg(#natmult(@x, @y))
#mult(#pos(@x), #0) → #0
#mult(#pos(@x), #neg(@y)) → #neg(#natmult(@x, @y))
#mult(#pos(@x), #pos(@y)) → #pos(#natmult(@x, @y))
#natmult(#0, @y) → #0
#natmult(#s(@x), @y) → #add(#pos(@y), #natmult(@x, @y))
#pred(#0) → #neg(#s(#0))
#pred(#neg(#s(@x))) → #neg(#s(#s(@x)))
#pred(#pos(#s(#0))) → #0
#pred(#pos(#s(#s(@x)))) → #pos(#s(@x))
#succ(#0) → #pos(#s(#0))
#succ(#neg(#s(#0))) → #0
#succ(#neg(#s(#s(@x)))) → #neg(#s(@x))
#succ(#pos(#s(@x))) → #pos(#s(#s(@x)))

Types:
#abs :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
#0 :: #0:#neg:#pos:#s::::nil
#neg :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
#pos :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
#s :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
*' :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
#mult :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
+' :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
#add :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
attach :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
attach#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
:: :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
attach#2 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
nil :: #0:#neg:#pos:#s::::nil
lineMult :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
lineMult#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
mult :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
m1 :: #0:#neg:#pos:#s::::nil
m2 :: #0:#neg:#pos:#s::::nil
m3 :: #0:#neg:#pos:#s::::nil
m4 :: #0:#neg:#pos:#s::::nil
makeBase :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
makeBase#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
mkBase :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
matrixMult :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
matrixMult' :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
transAcc :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
matrixMult'#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
matrixMult3 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
matrixMultList :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
matrixMultList#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
matrixMultOld :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
transpose :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
mkBase#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
mult#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
mult#2 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
split :: #0:#neg:#pos:#s::::nil → tuple#2
split#1 :: #0:#neg:#pos:#s::::nil → tuple#2
split#2 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → tuple#2
tuple#2 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → tuple#2
split#3 :: tuple#2 → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → tuple#2
transAcc#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
transpose#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
transpose#2 :: tuple#2 → #0:#neg:#pos:#s::::nil
transpose#3 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
transpose' :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
#pred :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
#succ :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
#natmult :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
hole_#0:#neg:#pos:#s::::nil1_5 :: #0:#neg:#pos:#s::::nil
hole_tuple#22_5 :: tuple#2
gen_#0:#neg:#pos:#s::::nil3_5 :: Nat → #0:#neg:#pos:#s::::nil

Generator Equations:
gen_#0:#neg:#pos:#s::::nil3_5(0) ⇔ #0
gen_#0:#neg:#pos:#s::::nil3_5(+(x, 1)) ⇔ #neg(gen_#0:#neg:#pos:#s::::nil3_5(x))

The following defined symbols remain to be analysed:
mult, attach, attach#1, lineMult, lineMult#1, matrixMult', transAcc, matrixMult'#1, transAcc#1

They will be analysed ascendingly in the following order:
attach = attach#1
attach < transAcc#1
lineMult = lineMult#1
lineMult < matrixMult'#1
mult < lineMult#1
mult = mult#1
matrixMult' = matrixMult'#1
transAcc = transAcc#1

(33) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol mult.

(34) Obligation:

Innermost TRS:
Rules:
#abs(#0) → #0
#abs(#neg(@x)) → #pos(@x)
#abs(#pos(@x)) → #pos(@x)
#abs(#s(@x)) → #pos(#s(@x))
*'(@x, @y) → #mult(@x, @y)
+'(@x, @y) → #add(@x, @y)
attach(@line, @m) → attach#1(@line, @m)
attach#1(::(@x, @xs), @m) → attach#2(@m, @x, @xs)
attach#1(nil, @m) → nil
attach#2(::(@l, @ls), @x, @xs) → ::(::(@x, @l), attach(@xs, @ls))
attach#2(nil, @x, @xs) → nil
lineMult(@l, @m2) → lineMult#1(@m2, @l)
lineMult#1(::(@x, @xs), @l) → ::(mult(@l, @x), lineMult(@l, @xs))
lineMult#1(nil, @l) → nil
m1 → ::(::(#abs(#pos(#s(#0))), ::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#0))))), nil))), ::(::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#0))))), ::(#abs(#pos(#s(#s(#s(#s(#0)))))), nil))), nil))
m2 → ::(::(#abs(#pos(#s(#0))), ::(#abs(#pos(#s(#s(#0)))), nil)), ::(::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#0))))), nil)), ::(::(#abs(#pos(#s(#s(#s(#s(#0)))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#0))))))), nil)), nil)))
m3 → ::(::(#abs(#pos(#s(#0))), ::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#0))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#0))))))), nil)))), ::(::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#0))))), ::(#abs(#pos(#s(#s(#s(#s(#0)))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#0))))))), nil)))), nil))
m4 → ::(::(#abs(#pos(#s(#0))), nil), ::(::(#abs(#pos(#s(#s(#0)))), nil), ::(::(#abs(#pos(#s(#s(#s(#0))))), nil), ::(::(#abs(#pos(#s(#s(#s(#s(#0)))))), nil), nil))))
makeBase(@m) → makeBase#1(@m)
makeBase#1(::(@l, @m')) → mkBase(@l)
makeBase#1(nil) → nil
matrixMult(@m1, @m2) → matrixMult'(@m1, transAcc(@m2, makeBase(@m2)))
matrixMult'(@m1, @m2) → matrixMult'#1(@m1, @m2)
matrixMult'#1(::(@l, @ls), @m2) → ::(lineMult(@l, @m2), matrixMult'(@ls, @m2))
matrixMult'#1(nil, @m2) → nil
matrixMult3(@m1, @m2, @m3) → matrixMult(matrixMult(@m1, @m2), @m3)
matrixMultList(@acc, @mm) → matrixMultList#1(@mm, @acc)
matrixMultList#1(::(@m, @ms), @acc) → matrixMultList(matrixMult(@acc, @m), @ms)
matrixMultList#1(nil, @acc) → @acc
matrixMultOld(@m1, @m2) → matrixMult'(@m1, transpose(@m2))
mkBase(@m) → mkBase#1(@m)
mkBase#1(::(@l, @m')) → ::(nil, mkBase(@m'))
mkBase#1(nil) → nil
mult(@l1, @l2) → mult#1(@l1, @l2)
mult#1(::(@x, @xs), @l2) → mult#2(@l2, @x, @xs)
mult#1(nil, @l2) → #abs(#0)
mult#2(::(@y, @ys), @x, @xs) → +'(*'(@x, @y), mult(@xs, @ys))
mult#2(nil, @x, @xs) → #abs(#0)
split(@m) → split#1(@m)
split#1(::(@l, @ls)) → split#2(@l, @ls)
split#1(nil) → tuple#2(nil, nil)
split#2(::(@x, @xs), @ls) → split#3(split(@ls), @x, @xs)
split#2(nil, @ls) → tuple#2(nil, nil)
split#3(tuple#2(@ys, @m'), @x, @xs) → tuple#2(::(@x, @ys), ::(@xs, @m'))
transAcc(@m, @base) → transAcc#1(@m, @base)
transAcc#1(::(@l, @m'), @base) → attach(@l, transAcc(@m', @base))
transAcc#1(nil, @base) → @base
transpose(@m) → transpose#1(@m, @m)
transpose#1(::(@xs, @xss), @m) → transpose#2(split(@m))
transpose#1(nil, @m) → nil
transpose#2(tuple#2(@l, @m')) → transpose#3(@m', @l)
transpose#3(::(@y, @ys), @l) → ::(@l, transpose(::(@y, @ys)))
transpose#3(nil, @l) → nil
transpose'(@m) → transAcc(@m, makeBase(@m))
#add(#0, @y) → @y
#add(#neg(#s(#0)), @y) → #pred(@y)
#add(#neg(#s(#s(@x))), @y) → #pred(#add(#pos(#s(@x)), @y))
#add(#pos(#s(#0)), @y) → #succ(@y)
#add(#pos(#s(#s(@x))), @y) → #succ(#add(#pos(#s(@x)), @y))
#mult(#0, #0) → #0
#mult(#0, #neg(@y)) → #0
#mult(#0, #pos(@y)) → #0
#mult(#neg(@x), #0) → #0
#mult(#neg(@x), #neg(@y)) → #pos(#natmult(@x, @y))
#mult(#neg(@x), #pos(@y)) → #neg(#natmult(@x, @y))
#mult(#pos(@x), #0) → #0
#mult(#pos(@x), #neg(@y)) → #neg(#natmult(@x, @y))
#mult(#pos(@x), #pos(@y)) → #pos(#natmult(@x, @y))
#natmult(#0, @y) → #0
#natmult(#s(@x), @y) → #add(#pos(@y), #natmult(@x, @y))
#pred(#0) → #neg(#s(#0))
#pred(#neg(#s(@x))) → #neg(#s(#s(@x)))
#pred(#pos(#s(#0))) → #0
#pred(#pos(#s(#s(@x)))) → #pos(#s(@x))
#succ(#0) → #pos(#s(#0))
#succ(#neg(#s(#0))) → #0
#succ(#neg(#s(#s(@x)))) → #neg(#s(@x))
#succ(#pos(#s(@x))) → #pos(#s(#s(@x)))

Types:
#abs :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
#0 :: #0:#neg:#pos:#s::::nil
#neg :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
#pos :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
#s :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
*' :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
#mult :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
+' :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
#add :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
attach :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
attach#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
:: :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
attach#2 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
nil :: #0:#neg:#pos:#s::::nil
lineMult :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
lineMult#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
mult :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
m1 :: #0:#neg:#pos:#s::::nil
m2 :: #0:#neg:#pos:#s::::nil
m3 :: #0:#neg:#pos:#s::::nil
m4 :: #0:#neg:#pos:#s::::nil
makeBase :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
makeBase#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
mkBase :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
matrixMult :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
matrixMult' :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
transAcc :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
matrixMult'#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
matrixMult3 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
matrixMultList :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
matrixMultList#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
matrixMultOld :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
transpose :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
mkBase#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
mult#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
mult#2 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
split :: #0:#neg:#pos:#s::::nil → tuple#2
split#1 :: #0:#neg:#pos:#s::::nil → tuple#2
split#2 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → tuple#2
tuple#2 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → tuple#2
split#3 :: tuple#2 → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → tuple#2
transAcc#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
transpose#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
transpose#2 :: tuple#2 → #0:#neg:#pos:#s::::nil
transpose#3 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
transpose' :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
#pred :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
#succ :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
#natmult :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
hole_#0:#neg:#pos:#s::::nil1_5 :: #0:#neg:#pos:#s::::nil
hole_tuple#22_5 :: tuple#2
gen_#0:#neg:#pos:#s::::nil3_5 :: Nat → #0:#neg:#pos:#s::::nil

Generator Equations:
gen_#0:#neg:#pos:#s::::nil3_5(0) ⇔ #0
gen_#0:#neg:#pos:#s::::nil3_5(+(x, 1)) ⇔ #neg(gen_#0:#neg:#pos:#s::::nil3_5(x))

The following defined symbols remain to be analysed:
lineMult#1, attach, attach#1, lineMult, matrixMult', transAcc, matrixMult'#1, transAcc#1

They will be analysed ascendingly in the following order:
attach = attach#1
attach < transAcc#1
lineMult = lineMult#1
lineMult < matrixMult'#1
matrixMult' = matrixMult'#1
transAcc = transAcc#1

(35) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol lineMult#1.

(36) Obligation:

Innermost TRS:
Rules:
#abs(#0) → #0
#abs(#neg(@x)) → #pos(@x)
#abs(#pos(@x)) → #pos(@x)
#abs(#s(@x)) → #pos(#s(@x))
*'(@x, @y) → #mult(@x, @y)
+'(@x, @y) → #add(@x, @y)
attach(@line, @m) → attach#1(@line, @m)
attach#1(::(@x, @xs), @m) → attach#2(@m, @x, @xs)
attach#1(nil, @m) → nil
attach#2(::(@l, @ls), @x, @xs) → ::(::(@x, @l), attach(@xs, @ls))
attach#2(nil, @x, @xs) → nil
lineMult(@l, @m2) → lineMult#1(@m2, @l)
lineMult#1(::(@x, @xs), @l) → ::(mult(@l, @x), lineMult(@l, @xs))
lineMult#1(nil, @l) → nil
m1 → ::(::(#abs(#pos(#s(#0))), ::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#0))))), nil))), ::(::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#0))))), ::(#abs(#pos(#s(#s(#s(#s(#0)))))), nil))), nil))
m2 → ::(::(#abs(#pos(#s(#0))), ::(#abs(#pos(#s(#s(#0)))), nil)), ::(::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#0))))), nil)), ::(::(#abs(#pos(#s(#s(#s(#s(#0)))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#0))))))), nil)), nil)))
m3 → ::(::(#abs(#pos(#s(#0))), ::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#0))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#0))))))), nil)))), ::(::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#0))))), ::(#abs(#pos(#s(#s(#s(#s(#0)))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#0))))))), nil)))), nil))
m4 → ::(::(#abs(#pos(#s(#0))), nil), ::(::(#abs(#pos(#s(#s(#0)))), nil), ::(::(#abs(#pos(#s(#s(#s(#0))))), nil), ::(::(#abs(#pos(#s(#s(#s(#s(#0)))))), nil), nil))))
makeBase(@m) → makeBase#1(@m)
makeBase#1(::(@l, @m')) → mkBase(@l)
makeBase#1(nil) → nil
matrixMult(@m1, @m2) → matrixMult'(@m1, transAcc(@m2, makeBase(@m2)))
matrixMult'(@m1, @m2) → matrixMult'#1(@m1, @m2)
matrixMult'#1(::(@l, @ls), @m2) → ::(lineMult(@l, @m2), matrixMult'(@ls, @m2))
matrixMult'#1(nil, @m2) → nil
matrixMult3(@m1, @m2, @m3) → matrixMult(matrixMult(@m1, @m2), @m3)
matrixMultList(@acc, @mm) → matrixMultList#1(@mm, @acc)
matrixMultList#1(::(@m, @ms), @acc) → matrixMultList(matrixMult(@acc, @m), @ms)
matrixMultList#1(nil, @acc) → @acc
matrixMultOld(@m1, @m2) → matrixMult'(@m1, transpose(@m2))
mkBase(@m) → mkBase#1(@m)
mkBase#1(::(@l, @m')) → ::(nil, mkBase(@m'))
mkBase#1(nil) → nil
mult(@l1, @l2) → mult#1(@l1, @l2)
mult#1(::(@x, @xs), @l2) → mult#2(@l2, @x, @xs)
mult#1(nil, @l2) → #abs(#0)
mult#2(::(@y, @ys), @x, @xs) → +'(*'(@x, @y), mult(@xs, @ys))
mult#2(nil, @x, @xs) → #abs(#0)
split(@m) → split#1(@m)
split#1(::(@l, @ls)) → split#2(@l, @ls)
split#1(nil) → tuple#2(nil, nil)
split#2(::(@x, @xs), @ls) → split#3(split(@ls), @x, @xs)
split#2(nil, @ls) → tuple#2(nil, nil)
split#3(tuple#2(@ys, @m'), @x, @xs) → tuple#2(::(@x, @ys), ::(@xs, @m'))
transAcc(@m, @base) → transAcc#1(@m, @base)
transAcc#1(::(@l, @m'), @base) → attach(@l, transAcc(@m', @base))
transAcc#1(nil, @base) → @base
transpose(@m) → transpose#1(@m, @m)
transpose#1(::(@xs, @xss), @m) → transpose#2(split(@m))
transpose#1(nil, @m) → nil
transpose#2(tuple#2(@l, @m')) → transpose#3(@m', @l)
transpose#3(::(@y, @ys), @l) → ::(@l, transpose(::(@y, @ys)))
transpose#3(nil, @l) → nil
transpose'(@m) → transAcc(@m, makeBase(@m))
#add(#0, @y) → @y
#add(#neg(#s(#0)), @y) → #pred(@y)
#add(#neg(#s(#s(@x))), @y) → #pred(#add(#pos(#s(@x)), @y))
#add(#pos(#s(#0)), @y) → #succ(@y)
#add(#pos(#s(#s(@x))), @y) → #succ(#add(#pos(#s(@x)), @y))
#mult(#0, #0) → #0
#mult(#0, #neg(@y)) → #0
#mult(#0, #pos(@y)) → #0
#mult(#neg(@x), #0) → #0
#mult(#neg(@x), #neg(@y)) → #pos(#natmult(@x, @y))
#mult(#neg(@x), #pos(@y)) → #neg(#natmult(@x, @y))
#mult(#pos(@x), #0) → #0
#mult(#pos(@x), #neg(@y)) → #neg(#natmult(@x, @y))
#mult(#pos(@x), #pos(@y)) → #pos(#natmult(@x, @y))
#natmult(#0, @y) → #0
#natmult(#s(@x), @y) → #add(#pos(@y), #natmult(@x, @y))
#pred(#0) → #neg(#s(#0))
#pred(#neg(#s(@x))) → #neg(#s(#s(@x)))
#pred(#pos(#s(#0))) → #0
#pred(#pos(#s(#s(@x)))) → #pos(#s(@x))
#succ(#0) → #pos(#s(#0))
#succ(#neg(#s(#0))) → #0
#succ(#neg(#s(#s(@x)))) → #neg(#s(@x))
#succ(#pos(#s(@x))) → #pos(#s(#s(@x)))

Types:
#abs :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
#0 :: #0:#neg:#pos:#s::::nil
#neg :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
#pos :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
#s :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
*' :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
#mult :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
+' :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
#add :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
attach :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
attach#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
:: :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
attach#2 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
nil :: #0:#neg:#pos:#s::::nil
lineMult :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
lineMult#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
mult :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
m1 :: #0:#neg:#pos:#s::::nil
m2 :: #0:#neg:#pos:#s::::nil
m3 :: #0:#neg:#pos:#s::::nil
m4 :: #0:#neg:#pos:#s::::nil
makeBase :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
makeBase#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
mkBase :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
matrixMult :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
matrixMult' :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
transAcc :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
matrixMult'#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
matrixMult3 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
matrixMultList :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
matrixMultList#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
matrixMultOld :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
transpose :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
mkBase#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
mult#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
mult#2 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
split :: #0:#neg:#pos:#s::::nil → tuple#2
split#1 :: #0:#neg:#pos:#s::::nil → tuple#2
split#2 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → tuple#2
tuple#2 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → tuple#2
split#3 :: tuple#2 → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → tuple#2
transAcc#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
transpose#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
transpose#2 :: tuple#2 → #0:#neg:#pos:#s::::nil
transpose#3 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
transpose' :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
#pred :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
#succ :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
#natmult :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
hole_#0:#neg:#pos:#s::::nil1_5 :: #0:#neg:#pos:#s::::nil
hole_tuple#22_5 :: tuple#2
gen_#0:#neg:#pos:#s::::nil3_5 :: Nat → #0:#neg:#pos:#s::::nil

Generator Equations:
gen_#0:#neg:#pos:#s::::nil3_5(0) ⇔ #0
gen_#0:#neg:#pos:#s::::nil3_5(+(x, 1)) ⇔ #neg(gen_#0:#neg:#pos:#s::::nil3_5(x))

The following defined symbols remain to be analysed:
lineMult, attach, attach#1, matrixMult', transAcc, matrixMult'#1, transAcc#1

They will be analysed ascendingly in the following order:
attach = attach#1
attach < transAcc#1
lineMult = lineMult#1
lineMult < matrixMult'#1
matrixMult' = matrixMult'#1
transAcc = transAcc#1

(37) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol lineMult.

(38) Obligation:

Innermost TRS:
Rules:
#abs(#0) → #0
#abs(#neg(@x)) → #pos(@x)
#abs(#pos(@x)) → #pos(@x)
#abs(#s(@x)) → #pos(#s(@x))
*'(@x, @y) → #mult(@x, @y)
+'(@x, @y) → #add(@x, @y)
attach(@line, @m) → attach#1(@line, @m)
attach#1(::(@x, @xs), @m) → attach#2(@m, @x, @xs)
attach#1(nil, @m) → nil
attach#2(::(@l, @ls), @x, @xs) → ::(::(@x, @l), attach(@xs, @ls))
attach#2(nil, @x, @xs) → nil
lineMult(@l, @m2) → lineMult#1(@m2, @l)
lineMult#1(::(@x, @xs), @l) → ::(mult(@l, @x), lineMult(@l, @xs))
lineMult#1(nil, @l) → nil
m1 → ::(::(#abs(#pos(#s(#0))), ::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#0))))), nil))), ::(::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#0))))), ::(#abs(#pos(#s(#s(#s(#s(#0)))))), nil))), nil))
m2 → ::(::(#abs(#pos(#s(#0))), ::(#abs(#pos(#s(#s(#0)))), nil)), ::(::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#0))))), nil)), ::(::(#abs(#pos(#s(#s(#s(#s(#0)))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#0))))))), nil)), nil)))
m3 → ::(::(#abs(#pos(#s(#0))), ::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#0))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#0))))))), nil)))), ::(::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#0))))), ::(#abs(#pos(#s(#s(#s(#s(#0)))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#0))))))), nil)))), nil))
m4 → ::(::(#abs(#pos(#s(#0))), nil), ::(::(#abs(#pos(#s(#s(#0)))), nil), ::(::(#abs(#pos(#s(#s(#s(#0))))), nil), ::(::(#abs(#pos(#s(#s(#s(#s(#0)))))), nil), nil))))
makeBase(@m) → makeBase#1(@m)
makeBase#1(::(@l, @m')) → mkBase(@l)
makeBase#1(nil) → nil
matrixMult(@m1, @m2) → matrixMult'(@m1, transAcc(@m2, makeBase(@m2)))
matrixMult'(@m1, @m2) → matrixMult'#1(@m1, @m2)
matrixMult'#1(::(@l, @ls), @m2) → ::(lineMult(@l, @m2), matrixMult'(@ls, @m2))
matrixMult'#1(nil, @m2) → nil
matrixMult3(@m1, @m2, @m3) → matrixMult(matrixMult(@m1, @m2), @m3)
matrixMultList(@acc, @mm) → matrixMultList#1(@mm, @acc)
matrixMultList#1(::(@m, @ms), @acc) → matrixMultList(matrixMult(@acc, @m), @ms)
matrixMultList#1(nil, @acc) → @acc
matrixMultOld(@m1, @m2) → matrixMult'(@m1, transpose(@m2))
mkBase(@m) → mkBase#1(@m)
mkBase#1(::(@l, @m')) → ::(nil, mkBase(@m'))
mkBase#1(nil) → nil
mult(@l1, @l2) → mult#1(@l1, @l2)
mult#1(::(@x, @xs), @l2) → mult#2(@l2, @x, @xs)
mult#1(nil, @l2) → #abs(#0)
mult#2(::(@y, @ys), @x, @xs) → +'(*'(@x, @y), mult(@xs, @ys))
mult#2(nil, @x, @xs) → #abs(#0)
split(@m) → split#1(@m)
split#1(::(@l, @ls)) → split#2(@l, @ls)
split#1(nil) → tuple#2(nil, nil)
split#2(::(@x, @xs), @ls) → split#3(split(@ls), @x, @xs)
split#2(nil, @ls) → tuple#2(nil, nil)
split#3(tuple#2(@ys, @m'), @x, @xs) → tuple#2(::(@x, @ys), ::(@xs, @m'))
transAcc(@m, @base) → transAcc#1(@m, @base)
transAcc#1(::(@l, @m'), @base) → attach(@l, transAcc(@m', @base))
transAcc#1(nil, @base) → @base
transpose(@m) → transpose#1(@m, @m)
transpose#1(::(@xs, @xss), @m) → transpose#2(split(@m))
transpose#1(nil, @m) → nil
transpose#2(tuple#2(@l, @m')) → transpose#3(@m', @l)
transpose#3(::(@y, @ys), @l) → ::(@l, transpose(::(@y, @ys)))
transpose#3(nil, @l) → nil
transpose'(@m) → transAcc(@m, makeBase(@m))
#add(#0, @y) → @y
#add(#neg(#s(#0)), @y) → #pred(@y)
#add(#neg(#s(#s(@x))), @y) → #pred(#add(#pos(#s(@x)), @y))
#add(#pos(#s(#0)), @y) → #succ(@y)
#add(#pos(#s(#s(@x))), @y) → #succ(#add(#pos(#s(@x)), @y))
#mult(#0, #0) → #0
#mult(#0, #neg(@y)) → #0
#mult(#0, #pos(@y)) → #0
#mult(#neg(@x), #0) → #0
#mult(#neg(@x), #neg(@y)) → #pos(#natmult(@x, @y))
#mult(#neg(@x), #pos(@y)) → #neg(#natmult(@x, @y))
#mult(#pos(@x), #0) → #0
#mult(#pos(@x), #neg(@y)) → #neg(#natmult(@x, @y))
#mult(#pos(@x), #pos(@y)) → #pos(#natmult(@x, @y))
#natmult(#0, @y) → #0
#natmult(#s(@x), @y) → #add(#pos(@y), #natmult(@x, @y))
#pred(#0) → #neg(#s(#0))
#pred(#neg(#s(@x))) → #neg(#s(#s(@x)))
#pred(#pos(#s(#0))) → #0
#pred(#pos(#s(#s(@x)))) → #pos(#s(@x))
#succ(#0) → #pos(#s(#0))
#succ(#neg(#s(#0))) → #0
#succ(#neg(#s(#s(@x)))) → #neg(#s(@x))
#succ(#pos(#s(@x))) → #pos(#s(#s(@x)))

Types:
#abs :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
#0 :: #0:#neg:#pos:#s::::nil
#neg :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
#pos :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
#s :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
*' :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
#mult :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
+' :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
#add :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
attach :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
attach#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
:: :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
attach#2 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
nil :: #0:#neg:#pos:#s::::nil
lineMult :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
lineMult#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
mult :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
m1 :: #0:#neg:#pos:#s::::nil
m2 :: #0:#neg:#pos:#s::::nil
m3 :: #0:#neg:#pos:#s::::nil
m4 :: #0:#neg:#pos:#s::::nil
makeBase :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
makeBase#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
mkBase :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
matrixMult :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
matrixMult' :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
transAcc :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
matrixMult'#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
matrixMult3 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
matrixMultList :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
matrixMultList#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
matrixMultOld :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
transpose :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
mkBase#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
mult#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
mult#2 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
split :: #0:#neg:#pos:#s::::nil → tuple#2
split#1 :: #0:#neg:#pos:#s::::nil → tuple#2
split#2 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → tuple#2
tuple#2 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → tuple#2
split#3 :: tuple#2 → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → tuple#2
transAcc#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
transpose#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
transpose#2 :: tuple#2 → #0:#neg:#pos:#s::::nil
transpose#3 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
transpose' :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
#pred :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
#succ :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
#natmult :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
hole_#0:#neg:#pos:#s::::nil1_5 :: #0:#neg:#pos:#s::::nil
hole_tuple#22_5 :: tuple#2
gen_#0:#neg:#pos:#s::::nil3_5 :: Nat → #0:#neg:#pos:#s::::nil

Generator Equations:
gen_#0:#neg:#pos:#s::::nil3_5(0) ⇔ #0
gen_#0:#neg:#pos:#s::::nil3_5(+(x, 1)) ⇔ #neg(gen_#0:#neg:#pos:#s::::nil3_5(x))

The following defined symbols remain to be analysed:
matrixMult'#1, attach, attach#1, matrixMult', transAcc, transAcc#1

They will be analysed ascendingly in the following order:
attach = attach#1
attach < transAcc#1
matrixMult' = matrixMult'#1
transAcc = transAcc#1

(39) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol matrixMult'#1.

(40) Obligation:

Innermost TRS:
Rules:
#abs(#0) → #0
#abs(#neg(@x)) → #pos(@x)
#abs(#pos(@x)) → #pos(@x)
#abs(#s(@x)) → #pos(#s(@x))
*'(@x, @y) → #mult(@x, @y)
+'(@x, @y) → #add(@x, @y)
attach(@line, @m) → attach#1(@line, @m)
attach#1(::(@x, @xs), @m) → attach#2(@m, @x, @xs)
attach#1(nil, @m) → nil
attach#2(::(@l, @ls), @x, @xs) → ::(::(@x, @l), attach(@xs, @ls))
attach#2(nil, @x, @xs) → nil
lineMult(@l, @m2) → lineMult#1(@m2, @l)
lineMult#1(::(@x, @xs), @l) → ::(mult(@l, @x), lineMult(@l, @xs))
lineMult#1(nil, @l) → nil
m1 → ::(::(#abs(#pos(#s(#0))), ::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#0))))), nil))), ::(::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#0))))), ::(#abs(#pos(#s(#s(#s(#s(#0)))))), nil))), nil))
m2 → ::(::(#abs(#pos(#s(#0))), ::(#abs(#pos(#s(#s(#0)))), nil)), ::(::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#0))))), nil)), ::(::(#abs(#pos(#s(#s(#s(#s(#0)))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#0))))))), nil)), nil)))
m3 → ::(::(#abs(#pos(#s(#0))), ::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#0))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#0))))))), nil)))), ::(::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#0))))), ::(#abs(#pos(#s(#s(#s(#s(#0)))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#0))))))), nil)))), nil))
m4 → ::(::(#abs(#pos(#s(#0))), nil), ::(::(#abs(#pos(#s(#s(#0)))), nil), ::(::(#abs(#pos(#s(#s(#s(#0))))), nil), ::(::(#abs(#pos(#s(#s(#s(#s(#0)))))), nil), nil))))
makeBase(@m) → makeBase#1(@m)
makeBase#1(::(@l, @m')) → mkBase(@l)
makeBase#1(nil) → nil
matrixMult(@m1, @m2) → matrixMult'(@m1, transAcc(@m2, makeBase(@m2)))
matrixMult'(@m1, @m2) → matrixMult'#1(@m1, @m2)
matrixMult'#1(::(@l, @ls), @m2) → ::(lineMult(@l, @m2), matrixMult'(@ls, @m2))
matrixMult'#1(nil, @m2) → nil
matrixMult3(@m1, @m2, @m3) → matrixMult(matrixMult(@m1, @m2), @m3)
matrixMultList(@acc, @mm) → matrixMultList#1(@mm, @acc)
matrixMultList#1(::(@m, @ms), @acc) → matrixMultList(matrixMult(@acc, @m), @ms)
matrixMultList#1(nil, @acc) → @acc
matrixMultOld(@m1, @m2) → matrixMult'(@m1, transpose(@m2))
mkBase(@m) → mkBase#1(@m)
mkBase#1(::(@l, @m')) → ::(nil, mkBase(@m'))
mkBase#1(nil) → nil
mult(@l1, @l2) → mult#1(@l1, @l2)
mult#1(::(@x, @xs), @l2) → mult#2(@l2, @x, @xs)
mult#1(nil, @l2) → #abs(#0)
mult#2(::(@y, @ys), @x, @xs) → +'(*'(@x, @y), mult(@xs, @ys))
mult#2(nil, @x, @xs) → #abs(#0)
split(@m) → split#1(@m)
split#1(::(@l, @ls)) → split#2(@l, @ls)
split#1(nil) → tuple#2(nil, nil)
split#2(::(@x, @xs), @ls) → split#3(split(@ls), @x, @xs)
split#2(nil, @ls) → tuple#2(nil, nil)
split#3(tuple#2(@ys, @m'), @x, @xs) → tuple#2(::(@x, @ys), ::(@xs, @m'))
transAcc(@m, @base) → transAcc#1(@m, @base)
transAcc#1(::(@l, @m'), @base) → attach(@l, transAcc(@m', @base))
transAcc#1(nil, @base) → @base
transpose(@m) → transpose#1(@m, @m)
transpose#1(::(@xs, @xss), @m) → transpose#2(split(@m))
transpose#1(nil, @m) → nil
transpose#2(tuple#2(@l, @m')) → transpose#3(@m', @l)
transpose#3(::(@y, @ys), @l) → ::(@l, transpose(::(@y, @ys)))
transpose#3(nil, @l) → nil
transpose'(@m) → transAcc(@m, makeBase(@m))
#add(#0, @y) → @y
#add(#neg(#s(#0)), @y) → #pred(@y)
#add(#neg(#s(#s(@x))), @y) → #pred(#add(#pos(#s(@x)), @y))
#add(#pos(#s(#0)), @y) → #succ(@y)
#add(#pos(#s(#s(@x))), @y) → #succ(#add(#pos(#s(@x)), @y))
#mult(#0, #0) → #0
#mult(#0, #neg(@y)) → #0
#mult(#0, #pos(@y)) → #0
#mult(#neg(@x), #0) → #0
#mult(#neg(@x), #neg(@y)) → #pos(#natmult(@x, @y))
#mult(#neg(@x), #pos(@y)) → #neg(#natmult(@x, @y))
#mult(#pos(@x), #0) → #0
#mult(#pos(@x), #neg(@y)) → #neg(#natmult(@x, @y))
#mult(#pos(@x), #pos(@y)) → #pos(#natmult(@x, @y))
#natmult(#0, @y) → #0
#natmult(#s(@x), @y) → #add(#pos(@y), #natmult(@x, @y))
#pred(#0) → #neg(#s(#0))
#pred(#neg(#s(@x))) → #neg(#s(#s(@x)))
#pred(#pos(#s(#0))) → #0
#pred(#pos(#s(#s(@x)))) → #pos(#s(@x))
#succ(#0) → #pos(#s(#0))
#succ(#neg(#s(#0))) → #0
#succ(#neg(#s(#s(@x)))) → #neg(#s(@x))
#succ(#pos(#s(@x))) → #pos(#s(#s(@x)))

Types:
#abs :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
#0 :: #0:#neg:#pos:#s::::nil
#neg :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
#pos :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
#s :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
*' :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
#mult :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
+' :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
#add :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
attach :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
attach#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
:: :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
attach#2 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
nil :: #0:#neg:#pos:#s::::nil
lineMult :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
lineMult#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
mult :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
m1 :: #0:#neg:#pos:#s::::nil
m2 :: #0:#neg:#pos:#s::::nil
m3 :: #0:#neg:#pos:#s::::nil
m4 :: #0:#neg:#pos:#s::::nil
makeBase :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
makeBase#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
mkBase :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
matrixMult :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
matrixMult' :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
transAcc :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
matrixMult'#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
matrixMult3 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
matrixMultList :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
matrixMultList#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
matrixMultOld :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
transpose :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
mkBase#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
mult#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
mult#2 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
split :: #0:#neg:#pos:#s::::nil → tuple#2
split#1 :: #0:#neg:#pos:#s::::nil → tuple#2
split#2 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → tuple#2
tuple#2 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → tuple#2
split#3 :: tuple#2 → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → tuple#2
transAcc#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
transpose#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
transpose#2 :: tuple#2 → #0:#neg:#pos:#s::::nil
transpose#3 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
transpose' :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
#pred :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
#succ :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
#natmult :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
hole_#0:#neg:#pos:#s::::nil1_5 :: #0:#neg:#pos:#s::::nil
hole_tuple#22_5 :: tuple#2
gen_#0:#neg:#pos:#s::::nil3_5 :: Nat → #0:#neg:#pos:#s::::nil

Generator Equations:
gen_#0:#neg:#pos:#s::::nil3_5(0) ⇔ #0
gen_#0:#neg:#pos:#s::::nil3_5(+(x, 1)) ⇔ #neg(gen_#0:#neg:#pos:#s::::nil3_5(x))

The following defined symbols remain to be analysed:
matrixMult', attach, attach#1, transAcc, transAcc#1

They will be analysed ascendingly in the following order:
attach = attach#1
attach < transAcc#1
matrixMult' = matrixMult'#1
transAcc = transAcc#1

(41) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol matrixMult'.

(42) Obligation:

Innermost TRS:
Rules:
#abs(#0) → #0
#abs(#neg(@x)) → #pos(@x)
#abs(#pos(@x)) → #pos(@x)
#abs(#s(@x)) → #pos(#s(@x))
*'(@x, @y) → #mult(@x, @y)
+'(@x, @y) → #add(@x, @y)
attach(@line, @m) → attach#1(@line, @m)
attach#1(::(@x, @xs), @m) → attach#2(@m, @x, @xs)
attach#1(nil, @m) → nil
attach#2(::(@l, @ls), @x, @xs) → ::(::(@x, @l), attach(@xs, @ls))
attach#2(nil, @x, @xs) → nil
lineMult(@l, @m2) → lineMult#1(@m2, @l)
lineMult#1(::(@x, @xs), @l) → ::(mult(@l, @x), lineMult(@l, @xs))
lineMult#1(nil, @l) → nil
m1 → ::(::(#abs(#pos(#s(#0))), ::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#0))))), nil))), ::(::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#0))))), ::(#abs(#pos(#s(#s(#s(#s(#0)))))), nil))), nil))
m2 → ::(::(#abs(#pos(#s(#0))), ::(#abs(#pos(#s(#s(#0)))), nil)), ::(::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#0))))), nil)), ::(::(#abs(#pos(#s(#s(#s(#s(#0)))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#0))))))), nil)), nil)))
m3 → ::(::(#abs(#pos(#s(#0))), ::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#0))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#0))))))), nil)))), ::(::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#0))))), ::(#abs(#pos(#s(#s(#s(#s(#0)))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#0))))))), nil)))), nil))
m4 → ::(::(#abs(#pos(#s(#0))), nil), ::(::(#abs(#pos(#s(#s(#0)))), nil), ::(::(#abs(#pos(#s(#s(#s(#0))))), nil), ::(::(#abs(#pos(#s(#s(#s(#s(#0)))))), nil), nil))))
makeBase(@m) → makeBase#1(@m)
makeBase#1(::(@l, @m')) → mkBase(@l)
makeBase#1(nil) → nil
matrixMult(@m1, @m2) → matrixMult'(@m1, transAcc(@m2, makeBase(@m2)))
matrixMult'(@m1, @m2) → matrixMult'#1(@m1, @m2)
matrixMult'#1(::(@l, @ls), @m2) → ::(lineMult(@l, @m2), matrixMult'(@ls, @m2))
matrixMult'#1(nil, @m2) → nil
matrixMult3(@m1, @m2, @m3) → matrixMult(matrixMult(@m1, @m2), @m3)
matrixMultList(@acc, @mm) → matrixMultList#1(@mm, @acc)
matrixMultList#1(::(@m, @ms), @acc) → matrixMultList(matrixMult(@acc, @m), @ms)
matrixMultList#1(nil, @acc) → @acc
matrixMultOld(@m1, @m2) → matrixMult'(@m1, transpose(@m2))
mkBase(@m) → mkBase#1(@m)
mkBase#1(::(@l, @m')) → ::(nil, mkBase(@m'))
mkBase#1(nil) → nil
mult(@l1, @l2) → mult#1(@l1, @l2)
mult#1(::(@x, @xs), @l2) → mult#2(@l2, @x, @xs)
mult#1(nil, @l2) → #abs(#0)
mult#2(::(@y, @ys), @x, @xs) → +'(*'(@x, @y), mult(@xs, @ys))
mult#2(nil, @x, @xs) → #abs(#0)
split(@m) → split#1(@m)
split#1(::(@l, @ls)) → split#2(@l, @ls)
split#1(nil) → tuple#2(nil, nil)
split#2(::(@x, @xs), @ls) → split#3(split(@ls), @x, @xs)
split#2(nil, @ls) → tuple#2(nil, nil)
split#3(tuple#2(@ys, @m'), @x, @xs) → tuple#2(::(@x, @ys), ::(@xs, @m'))
transAcc(@m, @base) → transAcc#1(@m, @base)
transAcc#1(::(@l, @m'), @base) → attach(@l, transAcc(@m', @base))
transAcc#1(nil, @base) → @base
transpose(@m) → transpose#1(@m, @m)
transpose#1(::(@xs, @xss), @m) → transpose#2(split(@m))
transpose#1(nil, @m) → nil
transpose#2(tuple#2(@l, @m')) → transpose#3(@m', @l)
transpose#3(::(@y, @ys), @l) → ::(@l, transpose(::(@y, @ys)))
transpose#3(nil, @l) → nil
transpose'(@m) → transAcc(@m, makeBase(@m))
#add(#0, @y) → @y
#add(#neg(#s(#0)), @y) → #pred(@y)
#add(#neg(#s(#s(@x))), @y) → #pred(#add(#pos(#s(@x)), @y))
#add(#pos(#s(#0)), @y) → #succ(@y)
#add(#pos(#s(#s(@x))), @y) → #succ(#add(#pos(#s(@x)), @y))
#mult(#0, #0) → #0
#mult(#0, #neg(@y)) → #0
#mult(#0, #pos(@y)) → #0
#mult(#neg(@x), #0) → #0
#mult(#neg(@x), #neg(@y)) → #pos(#natmult(@x, @y))
#mult(#neg(@x), #pos(@y)) → #neg(#natmult(@x, @y))
#mult(#pos(@x), #0) → #0
#mult(#pos(@x), #neg(@y)) → #neg(#natmult(@x, @y))
#mult(#pos(@x), #pos(@y)) → #pos(#natmult(@x, @y))
#natmult(#0, @y) → #0
#natmult(#s(@x), @y) → #add(#pos(@y), #natmult(@x, @y))
#pred(#0) → #neg(#s(#0))
#pred(#neg(#s(@x))) → #neg(#s(#s(@x)))
#pred(#pos(#s(#0))) → #0
#pred(#pos(#s(#s(@x)))) → #pos(#s(@x))
#succ(#0) → #pos(#s(#0))
#succ(#neg(#s(#0))) → #0
#succ(#neg(#s(#s(@x)))) → #neg(#s(@x))
#succ(#pos(#s(@x))) → #pos(#s(#s(@x)))

Types:
#abs :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
#0 :: #0:#neg:#pos:#s::::nil
#neg :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
#pos :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
#s :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
*' :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
#mult :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
+' :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
#add :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
attach :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
attach#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
:: :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
attach#2 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
nil :: #0:#neg:#pos:#s::::nil
lineMult :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
lineMult#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
mult :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
m1 :: #0:#neg:#pos:#s::::nil
m2 :: #0:#neg:#pos:#s::::nil
m3 :: #0:#neg:#pos:#s::::nil
m4 :: #0:#neg:#pos:#s::::nil
makeBase :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
makeBase#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
mkBase :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
matrixMult :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
matrixMult' :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
transAcc :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
matrixMult'#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
matrixMult3 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
matrixMultList :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
matrixMultList#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
matrixMultOld :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
transpose :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
mkBase#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
mult#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
mult#2 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
split :: #0:#neg:#pos:#s::::nil → tuple#2
split#1 :: #0:#neg:#pos:#s::::nil → tuple#2
split#2 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → tuple#2
tuple#2 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → tuple#2
split#3 :: tuple#2 → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → tuple#2
transAcc#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
transpose#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
transpose#2 :: tuple#2 → #0:#neg:#pos:#s::::nil
transpose#3 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
transpose' :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
#pred :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
#succ :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
#natmult :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
hole_#0:#neg:#pos:#s::::nil1_5 :: #0:#neg:#pos:#s::::nil
hole_tuple#22_5 :: tuple#2
gen_#0:#neg:#pos:#s::::nil3_5 :: Nat → #0:#neg:#pos:#s::::nil

Generator Equations:
gen_#0:#neg:#pos:#s::::nil3_5(0) ⇔ #0
gen_#0:#neg:#pos:#s::::nil3_5(+(x, 1)) ⇔ #neg(gen_#0:#neg:#pos:#s::::nil3_5(x))

The following defined symbols remain to be analysed:
attach#1, attach, transAcc, transAcc#1

They will be analysed ascendingly in the following order:
attach = attach#1
attach < transAcc#1
transAcc = transAcc#1

(43) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol attach#1.

(44) Obligation:

Innermost TRS:
Rules:
#abs(#0) → #0
#abs(#neg(@x)) → #pos(@x)
#abs(#pos(@x)) → #pos(@x)
#abs(#s(@x)) → #pos(#s(@x))
*'(@x, @y) → #mult(@x, @y)
+'(@x, @y) → #add(@x, @y)
attach(@line, @m) → attach#1(@line, @m)
attach#1(::(@x, @xs), @m) → attach#2(@m, @x, @xs)
attach#1(nil, @m) → nil
attach#2(::(@l, @ls), @x, @xs) → ::(::(@x, @l), attach(@xs, @ls))
attach#2(nil, @x, @xs) → nil
lineMult(@l, @m2) → lineMult#1(@m2, @l)
lineMult#1(::(@x, @xs), @l) → ::(mult(@l, @x), lineMult(@l, @xs))
lineMult#1(nil, @l) → nil
m1 → ::(::(#abs(#pos(#s(#0))), ::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#0))))), nil))), ::(::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#0))))), ::(#abs(#pos(#s(#s(#s(#s(#0)))))), nil))), nil))
m2 → ::(::(#abs(#pos(#s(#0))), ::(#abs(#pos(#s(#s(#0)))), nil)), ::(::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#0))))), nil)), ::(::(#abs(#pos(#s(#s(#s(#s(#0)))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#0))))))), nil)), nil)))
m3 → ::(::(#abs(#pos(#s(#0))), ::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#0))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#0))))))), nil)))), ::(::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#0))))), ::(#abs(#pos(#s(#s(#s(#s(#0)))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#0))))))), nil)))), nil))
m4 → ::(::(#abs(#pos(#s(#0))), nil), ::(::(#abs(#pos(#s(#s(#0)))), nil), ::(::(#abs(#pos(#s(#s(#s(#0))))), nil), ::(::(#abs(#pos(#s(#s(#s(#s(#0)))))), nil), nil))))
makeBase(@m) → makeBase#1(@m)
makeBase#1(::(@l, @m')) → mkBase(@l)
makeBase#1(nil) → nil
matrixMult(@m1, @m2) → matrixMult'(@m1, transAcc(@m2, makeBase(@m2)))
matrixMult'(@m1, @m2) → matrixMult'#1(@m1, @m2)
matrixMult'#1(::(@l, @ls), @m2) → ::(lineMult(@l, @m2), matrixMult'(@ls, @m2))
matrixMult'#1(nil, @m2) → nil
matrixMult3(@m1, @m2, @m3) → matrixMult(matrixMult(@m1, @m2), @m3)
matrixMultList(@acc, @mm) → matrixMultList#1(@mm, @acc)
matrixMultList#1(::(@m, @ms), @acc) → matrixMultList(matrixMult(@acc, @m), @ms)
matrixMultList#1(nil, @acc) → @acc
matrixMultOld(@m1, @m2) → matrixMult'(@m1, transpose(@m2))
mkBase(@m) → mkBase#1(@m)
mkBase#1(::(@l, @m')) → ::(nil, mkBase(@m'))
mkBase#1(nil) → nil
mult(@l1, @l2) → mult#1(@l1, @l2)
mult#1(::(@x, @xs), @l2) → mult#2(@l2, @x, @xs)
mult#1(nil, @l2) → #abs(#0)
mult#2(::(@y, @ys), @x, @xs) → +'(*'(@x, @y), mult(@xs, @ys))
mult#2(nil, @x, @xs) → #abs(#0)
split(@m) → split#1(@m)
split#1(::(@l, @ls)) → split#2(@l, @ls)
split#1(nil) → tuple#2(nil, nil)
split#2(::(@x, @xs), @ls) → split#3(split(@ls), @x, @xs)
split#2(nil, @ls) → tuple#2(nil, nil)
split#3(tuple#2(@ys, @m'), @x, @xs) → tuple#2(::(@x, @ys), ::(@xs, @m'))
transAcc(@m, @base) → transAcc#1(@m, @base)
transAcc#1(::(@l, @m'), @base) → attach(@l, transAcc(@m', @base))
transAcc#1(nil, @base) → @base
transpose(@m) → transpose#1(@m, @m)
transpose#1(::(@xs, @xss), @m) → transpose#2(split(@m))
transpose#1(nil, @m) → nil
transpose#2(tuple#2(@l, @m')) → transpose#3(@m', @l)
transpose#3(::(@y, @ys), @l) → ::(@l, transpose(::(@y, @ys)))
transpose#3(nil, @l) → nil
transpose'(@m) → transAcc(@m, makeBase(@m))
#add(#0, @y) → @y
#add(#neg(#s(#0)), @y) → #pred(@y)
#add(#neg(#s(#s(@x))), @y) → #pred(#add(#pos(#s(@x)), @y))
#add(#pos(#s(#0)), @y) → #succ(@y)
#add(#pos(#s(#s(@x))), @y) → #succ(#add(#pos(#s(@x)), @y))
#mult(#0, #0) → #0
#mult(#0, #neg(@y)) → #0
#mult(#0, #pos(@y)) → #0
#mult(#neg(@x), #0) → #0
#mult(#neg(@x), #neg(@y)) → #pos(#natmult(@x, @y))
#mult(#neg(@x), #pos(@y)) → #neg(#natmult(@x, @y))
#mult(#pos(@x), #0) → #0
#mult(#pos(@x), #neg(@y)) → #neg(#natmult(@x, @y))
#mult(#pos(@x), #pos(@y)) → #pos(#natmult(@x, @y))
#natmult(#0, @y) → #0
#natmult(#s(@x), @y) → #add(#pos(@y), #natmult(@x, @y))
#pred(#0) → #neg(#s(#0))
#pred(#neg(#s(@x))) → #neg(#s(#s(@x)))
#pred(#pos(#s(#0))) → #0
#pred(#pos(#s(#s(@x)))) → #pos(#s(@x))
#succ(#0) → #pos(#s(#0))
#succ(#neg(#s(#0))) → #0
#succ(#neg(#s(#s(@x)))) → #neg(#s(@x))
#succ(#pos(#s(@x))) → #pos(#s(#s(@x)))

Types:
#abs :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
#0 :: #0:#neg:#pos:#s::::nil
#neg :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
#pos :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
#s :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
*' :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
#mult :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
+' :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
#add :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
attach :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
attach#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
:: :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
attach#2 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
nil :: #0:#neg:#pos:#s::::nil
lineMult :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
lineMult#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
mult :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
m1 :: #0:#neg:#pos:#s::::nil
m2 :: #0:#neg:#pos:#s::::nil
m3 :: #0:#neg:#pos:#s::::nil
m4 :: #0:#neg:#pos:#s::::nil
makeBase :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
makeBase#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
mkBase :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
matrixMult :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
matrixMult' :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
transAcc :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
matrixMult'#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
matrixMult3 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
matrixMultList :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
matrixMultList#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
matrixMultOld :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
transpose :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
mkBase#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
mult#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
mult#2 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
split :: #0:#neg:#pos:#s::::nil → tuple#2
split#1 :: #0:#neg:#pos:#s::::nil → tuple#2
split#2 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → tuple#2
tuple#2 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → tuple#2
split#3 :: tuple#2 → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → tuple#2
transAcc#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
transpose#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
transpose#2 :: tuple#2 → #0:#neg:#pos:#s::::nil
transpose#3 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
transpose' :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
#pred :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
#succ :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
#natmult :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
hole_#0:#neg:#pos:#s::::nil1_5 :: #0:#neg:#pos:#s::::nil
hole_tuple#22_5 :: tuple#2
gen_#0:#neg:#pos:#s::::nil3_5 :: Nat → #0:#neg:#pos:#s::::nil

Generator Equations:
gen_#0:#neg:#pos:#s::::nil3_5(0) ⇔ #0
gen_#0:#neg:#pos:#s::::nil3_5(+(x, 1)) ⇔ #neg(gen_#0:#neg:#pos:#s::::nil3_5(x))

The following defined symbols remain to be analysed:
attach, transAcc, transAcc#1

They will be analysed ascendingly in the following order:
attach = attach#1
attach < transAcc#1
transAcc = transAcc#1

(45) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol attach.

(46) Obligation:

Innermost TRS:
Rules:
#abs(#0) → #0
#abs(#neg(@x)) → #pos(@x)
#abs(#pos(@x)) → #pos(@x)
#abs(#s(@x)) → #pos(#s(@x))
*'(@x, @y) → #mult(@x, @y)
+'(@x, @y) → #add(@x, @y)
attach(@line, @m) → attach#1(@line, @m)
attach#1(::(@x, @xs), @m) → attach#2(@m, @x, @xs)
attach#1(nil, @m) → nil
attach#2(::(@l, @ls), @x, @xs) → ::(::(@x, @l), attach(@xs, @ls))
attach#2(nil, @x, @xs) → nil
lineMult(@l, @m2) → lineMult#1(@m2, @l)
lineMult#1(::(@x, @xs), @l) → ::(mult(@l, @x), lineMult(@l, @xs))
lineMult#1(nil, @l) → nil
m1 → ::(::(#abs(#pos(#s(#0))), ::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#0))))), nil))), ::(::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#0))))), ::(#abs(#pos(#s(#s(#s(#s(#0)))))), nil))), nil))
m2 → ::(::(#abs(#pos(#s(#0))), ::(#abs(#pos(#s(#s(#0)))), nil)), ::(::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#0))))), nil)), ::(::(#abs(#pos(#s(#s(#s(#s(#0)))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#0))))))), nil)), nil)))
m3 → ::(::(#abs(#pos(#s(#0))), ::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#0))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#0))))))), nil)))), ::(::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#0))))), ::(#abs(#pos(#s(#s(#s(#s(#0)))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#0))))))), nil)))), nil))
m4 → ::(::(#abs(#pos(#s(#0))), nil), ::(::(#abs(#pos(#s(#s(#0)))), nil), ::(::(#abs(#pos(#s(#s(#s(#0))))), nil), ::(::(#abs(#pos(#s(#s(#s(#s(#0)))))), nil), nil))))
makeBase(@m) → makeBase#1(@m)
makeBase#1(::(@l, @m')) → mkBase(@l)
makeBase#1(nil) → nil
matrixMult(@m1, @m2) → matrixMult'(@m1, transAcc(@m2, makeBase(@m2)))
matrixMult'(@m1, @m2) → matrixMult'#1(@m1, @m2)
matrixMult'#1(::(@l, @ls), @m2) → ::(lineMult(@l, @m2), matrixMult'(@ls, @m2))
matrixMult'#1(nil, @m2) → nil
matrixMult3(@m1, @m2, @m3) → matrixMult(matrixMult(@m1, @m2), @m3)
matrixMultList(@acc, @mm) → matrixMultList#1(@mm, @acc)
matrixMultList#1(::(@m, @ms), @acc) → matrixMultList(matrixMult(@acc, @m), @ms)
matrixMultList#1(nil, @acc) → @acc
matrixMultOld(@m1, @m2) → matrixMult'(@m1, transpose(@m2))
mkBase(@m) → mkBase#1(@m)
mkBase#1(::(@l, @m')) → ::(nil, mkBase(@m'))
mkBase#1(nil) → nil
mult(@l1, @l2) → mult#1(@l1, @l2)
mult#1(::(@x, @xs), @l2) → mult#2(@l2, @x, @xs)
mult#1(nil, @l2) → #abs(#0)
mult#2(::(@y, @ys), @x, @xs) → +'(*'(@x, @y), mult(@xs, @ys))
mult#2(nil, @x, @xs) → #abs(#0)
split(@m) → split#1(@m)
split#1(::(@l, @ls)) → split#2(@l, @ls)
split#1(nil) → tuple#2(nil, nil)
split#2(::(@x, @xs), @ls) → split#3(split(@ls), @x, @xs)
split#2(nil, @ls) → tuple#2(nil, nil)
split#3(tuple#2(@ys, @m'), @x, @xs) → tuple#2(::(@x, @ys), ::(@xs, @m'))
transAcc(@m, @base) → transAcc#1(@m, @base)
transAcc#1(::(@l, @m'), @base) → attach(@l, transAcc(@m', @base))
transAcc#1(nil, @base) → @base
transpose(@m) → transpose#1(@m, @m)
transpose#1(::(@xs, @xss), @m) → transpose#2(split(@m))
transpose#1(nil, @m) → nil
transpose#2(tuple#2(@l, @m')) → transpose#3(@m', @l)
transpose#3(::(@y, @ys), @l) → ::(@l, transpose(::(@y, @ys)))
transpose#3(nil, @l) → nil
transpose'(@m) → transAcc(@m, makeBase(@m))
#add(#0, @y) → @y
#add(#neg(#s(#0)), @y) → #pred(@y)
#add(#neg(#s(#s(@x))), @y) → #pred(#add(#pos(#s(@x)), @y))
#add(#pos(#s(#0)), @y) → #succ(@y)
#add(#pos(#s(#s(@x))), @y) → #succ(#add(#pos(#s(@x)), @y))
#mult(#0, #0) → #0
#mult(#0, #neg(@y)) → #0
#mult(#0, #pos(@y)) → #0
#mult(#neg(@x), #0) → #0
#mult(#neg(@x), #neg(@y)) → #pos(#natmult(@x, @y))
#mult(#neg(@x), #pos(@y)) → #neg(#natmult(@x, @y))
#mult(#pos(@x), #0) → #0
#mult(#pos(@x), #neg(@y)) → #neg(#natmult(@x, @y))
#mult(#pos(@x), #pos(@y)) → #pos(#natmult(@x, @y))
#natmult(#0, @y) → #0
#natmult(#s(@x), @y) → #add(#pos(@y), #natmult(@x, @y))
#pred(#0) → #neg(#s(#0))
#pred(#neg(#s(@x))) → #neg(#s(#s(@x)))
#pred(#pos(#s(#0))) → #0
#pred(#pos(#s(#s(@x)))) → #pos(#s(@x))
#succ(#0) → #pos(#s(#0))
#succ(#neg(#s(#0))) → #0
#succ(#neg(#s(#s(@x)))) → #neg(#s(@x))
#succ(#pos(#s(@x))) → #pos(#s(#s(@x)))

Types:
#abs :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
#0 :: #0:#neg:#pos:#s::::nil
#neg :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
#pos :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
#s :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
*' :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
#mult :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
+' :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
#add :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
attach :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
attach#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
:: :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
attach#2 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
nil :: #0:#neg:#pos:#s::::nil
lineMult :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
lineMult#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
mult :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
m1 :: #0:#neg:#pos:#s::::nil
m2 :: #0:#neg:#pos:#s::::nil
m3 :: #0:#neg:#pos:#s::::nil
m4 :: #0:#neg:#pos:#s::::nil
makeBase :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
makeBase#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
mkBase :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
matrixMult :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
matrixMult' :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
transAcc :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
matrixMult'#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
matrixMult3 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
matrixMultList :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
matrixMultList#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
matrixMultOld :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
transpose :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
mkBase#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
mult#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
mult#2 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
split :: #0:#neg:#pos:#s::::nil → tuple#2
split#1 :: #0:#neg:#pos:#s::::nil → tuple#2
split#2 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → tuple#2
tuple#2 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → tuple#2
split#3 :: tuple#2 → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → tuple#2
transAcc#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
transpose#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
transpose#2 :: tuple#2 → #0:#neg:#pos:#s::::nil
transpose#3 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
transpose' :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
#pred :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
#succ :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
#natmult :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
hole_#0:#neg:#pos:#s::::nil1_5 :: #0:#neg:#pos:#s::::nil
hole_tuple#22_5 :: tuple#2
gen_#0:#neg:#pos:#s::::nil3_5 :: Nat → #0:#neg:#pos:#s::::nil

Generator Equations:
gen_#0:#neg:#pos:#s::::nil3_5(0) ⇔ #0
gen_#0:#neg:#pos:#s::::nil3_5(+(x, 1)) ⇔ #neg(gen_#0:#neg:#pos:#s::::nil3_5(x))

The following defined symbols remain to be analysed:
transAcc#1, transAcc

They will be analysed ascendingly in the following order:
transAcc = transAcc#1

(47) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol transAcc#1.

(48) Obligation:

Innermost TRS:
Rules:
#abs(#0) → #0
#abs(#neg(@x)) → #pos(@x)
#abs(#pos(@x)) → #pos(@x)
#abs(#s(@x)) → #pos(#s(@x))
*'(@x, @y) → #mult(@x, @y)
+'(@x, @y) → #add(@x, @y)
attach(@line, @m) → attach#1(@line, @m)
attach#1(::(@x, @xs), @m) → attach#2(@m, @x, @xs)
attach#1(nil, @m) → nil
attach#2(::(@l, @ls), @x, @xs) → ::(::(@x, @l), attach(@xs, @ls))
attach#2(nil, @x, @xs) → nil
lineMult(@l, @m2) → lineMult#1(@m2, @l)
lineMult#1(::(@x, @xs), @l) → ::(mult(@l, @x), lineMult(@l, @xs))
lineMult#1(nil, @l) → nil
m1 → ::(::(#abs(#pos(#s(#0))), ::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#0))))), nil))), ::(::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#0))))), ::(#abs(#pos(#s(#s(#s(#s(#0)))))), nil))), nil))
m2 → ::(::(#abs(#pos(#s(#0))), ::(#abs(#pos(#s(#s(#0)))), nil)), ::(::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#0))))), nil)), ::(::(#abs(#pos(#s(#s(#s(#s(#0)))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#0))))))), nil)), nil)))
m3 → ::(::(#abs(#pos(#s(#0))), ::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#0))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#0))))))), nil)))), ::(::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#0))))), ::(#abs(#pos(#s(#s(#s(#s(#0)))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#0))))))), nil)))), nil))
m4 → ::(::(#abs(#pos(#s(#0))), nil), ::(::(#abs(#pos(#s(#s(#0)))), nil), ::(::(#abs(#pos(#s(#s(#s(#0))))), nil), ::(::(#abs(#pos(#s(#s(#s(#s(#0)))))), nil), nil))))
makeBase(@m) → makeBase#1(@m)
makeBase#1(::(@l, @m')) → mkBase(@l)
makeBase#1(nil) → nil
matrixMult(@m1, @m2) → matrixMult'(@m1, transAcc(@m2, makeBase(@m2)))
matrixMult'(@m1, @m2) → matrixMult'#1(@m1, @m2)
matrixMult'#1(::(@l, @ls), @m2) → ::(lineMult(@l, @m2), matrixMult'(@ls, @m2))
matrixMult'#1(nil, @m2) → nil
matrixMult3(@m1, @m2, @m3) → matrixMult(matrixMult(@m1, @m2), @m3)
matrixMultList(@acc, @mm) → matrixMultList#1(@mm, @acc)
matrixMultList#1(::(@m, @ms), @acc) → matrixMultList(matrixMult(@acc, @m), @ms)
matrixMultList#1(nil, @acc) → @acc
matrixMultOld(@m1, @m2) → matrixMult'(@m1, transpose(@m2))
mkBase(@m) → mkBase#1(@m)
mkBase#1(::(@l, @m')) → ::(nil, mkBase(@m'))
mkBase#1(nil) → nil
mult(@l1, @l2) → mult#1(@l1, @l2)
mult#1(::(@x, @xs), @l2) → mult#2(@l2, @x, @xs)
mult#1(nil, @l2) → #abs(#0)
mult#2(::(@y, @ys), @x, @xs) → +'(*'(@x, @y), mult(@xs, @ys))
mult#2(nil, @x, @xs) → #abs(#0)
split(@m) → split#1(@m)
split#1(::(@l, @ls)) → split#2(@l, @ls)
split#1(nil) → tuple#2(nil, nil)
split#2(::(@x, @xs), @ls) → split#3(split(@ls), @x, @xs)
split#2(nil, @ls) → tuple#2(nil, nil)
split#3(tuple#2(@ys, @m'), @x, @xs) → tuple#2(::(@x, @ys), ::(@xs, @m'))
transAcc(@m, @base) → transAcc#1(@m, @base)
transAcc#1(::(@l, @m'), @base) → attach(@l, transAcc(@m', @base))
transAcc#1(nil, @base) → @base
transpose(@m) → transpose#1(@m, @m)
transpose#1(::(@xs, @xss), @m) → transpose#2(split(@m))
transpose#1(nil, @m) → nil
transpose#2(tuple#2(@l, @m')) → transpose#3(@m', @l)
transpose#3(::(@y, @ys), @l) → ::(@l, transpose(::(@y, @ys)))
transpose#3(nil, @l) → nil
transpose'(@m) → transAcc(@m, makeBase(@m))
#add(#0, @y) → @y
#add(#neg(#s(#0)), @y) → #pred(@y)
#add(#neg(#s(#s(@x))), @y) → #pred(#add(#pos(#s(@x)), @y))
#add(#pos(#s(#0)), @y) → #succ(@y)
#add(#pos(#s(#s(@x))), @y) → #succ(#add(#pos(#s(@x)), @y))
#mult(#0, #0) → #0
#mult(#0, #neg(@y)) → #0
#mult(#0, #pos(@y)) → #0
#mult(#neg(@x), #0) → #0
#mult(#neg(@x), #neg(@y)) → #pos(#natmult(@x, @y))
#mult(#neg(@x), #pos(@y)) → #neg(#natmult(@x, @y))
#mult(#pos(@x), #0) → #0
#mult(#pos(@x), #neg(@y)) → #neg(#natmult(@x, @y))
#mult(#pos(@x), #pos(@y)) → #pos(#natmult(@x, @y))
#natmult(#0, @y) → #0
#natmult(#s(@x), @y) → #add(#pos(@y), #natmult(@x, @y))
#pred(#0) → #neg(#s(#0))
#pred(#neg(#s(@x))) → #neg(#s(#s(@x)))
#pred(#pos(#s(#0))) → #0
#pred(#pos(#s(#s(@x)))) → #pos(#s(@x))
#succ(#0) → #pos(#s(#0))
#succ(#neg(#s(#0))) → #0
#succ(#neg(#s(#s(@x)))) → #neg(#s(@x))
#succ(#pos(#s(@x))) → #pos(#s(#s(@x)))

Types:
#abs :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
#0 :: #0:#neg:#pos:#s::::nil
#neg :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
#pos :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
#s :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
*' :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
#mult :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
+' :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
#add :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
attach :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
attach#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
:: :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
attach#2 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
nil :: #0:#neg:#pos:#s::::nil
lineMult :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
lineMult#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
mult :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
m1 :: #0:#neg:#pos:#s::::nil
m2 :: #0:#neg:#pos:#s::::nil
m3 :: #0:#neg:#pos:#s::::nil
m4 :: #0:#neg:#pos:#s::::nil
makeBase :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
makeBase#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
mkBase :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
matrixMult :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
matrixMult' :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
transAcc :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
matrixMult'#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
matrixMult3 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
matrixMultList :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
matrixMultList#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
matrixMultOld :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
transpose :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
mkBase#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
mult#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
mult#2 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
split :: #0:#neg:#pos:#s::::nil → tuple#2
split#1 :: #0:#neg:#pos:#s::::nil → tuple#2
split#2 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → tuple#2
tuple#2 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → tuple#2
split#3 :: tuple#2 → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → tuple#2
transAcc#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
transpose#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
transpose#2 :: tuple#2 → #0:#neg:#pos:#s::::nil
transpose#3 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
transpose' :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
#pred :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
#succ :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
#natmult :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
hole_#0:#neg:#pos:#s::::nil1_5 :: #0:#neg:#pos:#s::::nil
hole_tuple#22_5 :: tuple#2
gen_#0:#neg:#pos:#s::::nil3_5 :: Nat → #0:#neg:#pos:#s::::nil

Generator Equations:
gen_#0:#neg:#pos:#s::::nil3_5(0) ⇔ #0
gen_#0:#neg:#pos:#s::::nil3_5(+(x, 1)) ⇔ #neg(gen_#0:#neg:#pos:#s::::nil3_5(x))

The following defined symbols remain to be analysed:
transAcc

They will be analysed ascendingly in the following order:
transAcc = transAcc#1

(49) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol transAcc.

(50) Obligation:

Innermost TRS:
Rules:
#abs(#0) → #0
#abs(#neg(@x)) → #pos(@x)
#abs(#pos(@x)) → #pos(@x)
#abs(#s(@x)) → #pos(#s(@x))
*'(@x, @y) → #mult(@x, @y)
+'(@x, @y) → #add(@x, @y)
attach(@line, @m) → attach#1(@line, @m)
attach#1(::(@x, @xs), @m) → attach#2(@m, @x, @xs)
attach#1(nil, @m) → nil
attach#2(::(@l, @ls), @x, @xs) → ::(::(@x, @l), attach(@xs, @ls))
attach#2(nil, @x, @xs) → nil
lineMult(@l, @m2) → lineMult#1(@m2, @l)
lineMult#1(::(@x, @xs), @l) → ::(mult(@l, @x), lineMult(@l, @xs))
lineMult#1(nil, @l) → nil
m1 → ::(::(#abs(#pos(#s(#0))), ::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#0))))), nil))), ::(::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#0))))), ::(#abs(#pos(#s(#s(#s(#s(#0)))))), nil))), nil))
m2 → ::(::(#abs(#pos(#s(#0))), ::(#abs(#pos(#s(#s(#0)))), nil)), ::(::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#0))))), nil)), ::(::(#abs(#pos(#s(#s(#s(#s(#0)))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#0))))))), nil)), nil)))
m3 → ::(::(#abs(#pos(#s(#0))), ::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#0))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#0))))))), nil)))), ::(::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#0))))), ::(#abs(#pos(#s(#s(#s(#s(#0)))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#0))))))), nil)))), nil))
m4 → ::(::(#abs(#pos(#s(#0))), nil), ::(::(#abs(#pos(#s(#s(#0)))), nil), ::(::(#abs(#pos(#s(#s(#s(#0))))), nil), ::(::(#abs(#pos(#s(#s(#s(#s(#0)))))), nil), nil))))
makeBase(@m) → makeBase#1(@m)
makeBase#1(::(@l, @m')) → mkBase(@l)
makeBase#1(nil) → nil
matrixMult(@m1, @m2) → matrixMult'(@m1, transAcc(@m2, makeBase(@m2)))
matrixMult'(@m1, @m2) → matrixMult'#1(@m1, @m2)
matrixMult'#1(::(@l, @ls), @m2) → ::(lineMult(@l, @m2), matrixMult'(@ls, @m2))
matrixMult'#1(nil, @m2) → nil
matrixMult3(@m1, @m2, @m3) → matrixMult(matrixMult(@m1, @m2), @m3)
matrixMultList(@acc, @mm) → matrixMultList#1(@mm, @acc)
matrixMultList#1(::(@m, @ms), @acc) → matrixMultList(matrixMult(@acc, @m), @ms)
matrixMultList#1(nil, @acc) → @acc
matrixMultOld(@m1, @m2) → matrixMult'(@m1, transpose(@m2))
mkBase(@m) → mkBase#1(@m)
mkBase#1(::(@l, @m')) → ::(nil, mkBase(@m'))
mkBase#1(nil) → nil
mult(@l1, @l2) → mult#1(@l1, @l2)
mult#1(::(@x, @xs), @l2) → mult#2(@l2, @x, @xs)
mult#1(nil, @l2) → #abs(#0)
mult#2(::(@y, @ys), @x, @xs) → +'(*'(@x, @y), mult(@xs, @ys))
mult#2(nil, @x, @xs) → #abs(#0)
split(@m) → split#1(@m)
split#1(::(@l, @ls)) → split#2(@l, @ls)
split#1(nil) → tuple#2(nil, nil)
split#2(::(@x, @xs), @ls) → split#3(split(@ls), @x, @xs)
split#2(nil, @ls) → tuple#2(nil, nil)
split#3(tuple#2(@ys, @m'), @x, @xs) → tuple#2(::(@x, @ys), ::(@xs, @m'))
transAcc(@m, @base) → transAcc#1(@m, @base)
transAcc#1(::(@l, @m'), @base) → attach(@l, transAcc(@m', @base))
transAcc#1(nil, @base) → @base
transpose(@m) → transpose#1(@m, @m)
transpose#1(::(@xs, @xss), @m) → transpose#2(split(@m))
transpose#1(nil, @m) → nil
transpose#2(tuple#2(@l, @m')) → transpose#3(@m', @l)
transpose#3(::(@y, @ys), @l) → ::(@l, transpose(::(@y, @ys)))
transpose#3(nil, @l) → nil
transpose'(@m) → transAcc(@m, makeBase(@m))
#add(#0, @y) → @y
#add(#neg(#s(#0)), @y) → #pred(@y)
#add(#neg(#s(#s(@x))), @y) → #pred(#add(#pos(#s(@x)), @y))
#add(#pos(#s(#0)), @y) → #succ(@y)
#add(#pos(#s(#s(@x))), @y) → #succ(#add(#pos(#s(@x)), @y))
#mult(#0, #0) → #0
#mult(#0, #neg(@y)) → #0
#mult(#0, #pos(@y)) → #0
#mult(#neg(@x), #0) → #0
#mult(#neg(@x), #neg(@y)) → #pos(#natmult(@x, @y))
#mult(#neg(@x), #pos(@y)) → #neg(#natmult(@x, @y))
#mult(#pos(@x), #0) → #0
#mult(#pos(@x), #neg(@y)) → #neg(#natmult(@x, @y))
#mult(#pos(@x), #pos(@y)) → #pos(#natmult(@x, @y))
#natmult(#0, @y) → #0
#natmult(#s(@x), @y) → #add(#pos(@y), #natmult(@x, @y))
#pred(#0) → #neg(#s(#0))
#pred(#neg(#s(@x))) → #neg(#s(#s(@x)))
#pred(#pos(#s(#0))) → #0
#pred(#pos(#s(#s(@x)))) → #pos(#s(@x))
#succ(#0) → #pos(#s(#0))
#succ(#neg(#s(#0))) → #0
#succ(#neg(#s(#s(@x)))) → #neg(#s(@x))
#succ(#pos(#s(@x))) → #pos(#s(#s(@x)))

Types:
#abs :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
#0 :: #0:#neg:#pos:#s::::nil
#neg :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
#pos :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
#s :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
*' :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
#mult :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
+' :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
#add :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
attach :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
attach#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
:: :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
attach#2 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
nil :: #0:#neg:#pos:#s::::nil
lineMult :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
lineMult#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
mult :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
m1 :: #0:#neg:#pos:#s::::nil
m2 :: #0:#neg:#pos:#s::::nil
m3 :: #0:#neg:#pos:#s::::nil
m4 :: #0:#neg:#pos:#s::::nil
makeBase :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
makeBase#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
mkBase :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
matrixMult :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
matrixMult' :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
transAcc :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
matrixMult'#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
matrixMult3 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
matrixMultList :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
matrixMultList#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
matrixMultOld :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
transpose :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
mkBase#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
mult#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
mult#2 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
split :: #0:#neg:#pos:#s::::nil → tuple#2
split#1 :: #0:#neg:#pos:#s::::nil → tuple#2
split#2 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → tuple#2
tuple#2 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → tuple#2
split#3 :: tuple#2 → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → tuple#2
transAcc#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
transpose#1 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
transpose#2 :: tuple#2 → #0:#neg:#pos:#s::::nil
transpose#3 :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
transpose' :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
#pred :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
#succ :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
#natmult :: #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil → #0:#neg:#pos:#s::::nil
hole_#0:#neg:#pos:#s::::nil1_5 :: #0:#neg:#pos:#s::::nil
hole_tuple#22_5 :: tuple#2
gen_#0:#neg:#pos:#s::::nil3_5 :: Nat → #0:#neg:#pos:#s::::nil

Generator Equations:
gen_#0:#neg:#pos:#s::::nil3_5(0) ⇔ #0
gen_#0:#neg:#pos:#s::::nil3_5(+(x, 1)) ⇔ #neg(gen_#0:#neg:#pos:#s::::nil3_5(x))

No more defined symbols left to analyse.